:: deftheorem defines additive VECTSP_1:def 19 :
for G, H being non empty addMagma
for f being Function of G,H holds
( f is additive iff for x, y being Element of G holds f . (x + y) = (f . x) + (f . y) );