:: deftheorem defines + AOFA_I00:def 12 :
for X being non empty set
for t1, t2, b₄ being Function of X,INT holds
( b₄ = t1 + t2 iff for s being Element of X holds b₄ . s = (t1 . s) + (t2 . s) );