:: deftheorem Def1 defines additive PDIFF_6:def 1 :
for n, m being Nat
for IT being Function of (REAL m),(REAL n) holds
( IT is additive iff for x, y being Element of REAL m holds IT . (x + y) = (IT . x) + (IT . y) );