:: deftheorem Def2 defines Variable AOFA_I00:def 2 :
for X, Y, Z being set
for f being Function of [:(Funcs (X,INT)),Y:],Z
for b₅ being Element of X holds
( b₅ is Variable of f iff verum );