:: deftheorem Def18 defines . AOFA_I00:def 18 :
for X being non empty set
for x being Element of X
for b₃ being INT-Expression of X holds
( b₃ = . x iff for s being Element of Funcs (X,INT) holds b₃ . s = s . x );