As you know, given A, the function can be extended to a function from the set of all terms to |A|. In particular, A associates some function to a unary functional symbol and some function to a binary predicate symbol . Then , and iff .

By definition of , if , then . Therefore,

iff

iff

iff

iff

iff