:: deftheorem Def11 defines - AOFA_I00:def 11 :
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) );