:: deftheorem defines - AOFA_I00:def 9 :
for X being non empty set
for f being Function of X,INT
for x being Integer
for b₄ being Function of X,INT holds
( b₄ = f - x iff for s being Element of X holds b₄ . s = (f . s) - x );