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