theorem Th12: :: PDIFF_6:12

for n, m being Nat
for f being Function of (REAL m),(REAL n)
for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds
( f is additive iff g is additive )