:: deftheorem Def3 defines + SUPINF_2:def 3 :
for X being non empty set
for Y, Z being non empty Subset of ExtREAL
for F being Function of X,Y
for G being Function of X,Z
for b₆ being Function of X,(Y + Z) holds
( b₆ = F + G iff for x being Element of X holds b₆ . x = (F . x) + (G . x) );