let m, n be Element of NAT ; :: thesis: 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 )
let f be Function of (REAL m),(REAL n); :: thesis: for g being Function of (REAL-NS m),(REAL-NS n) st f = g holds
( f is additive iff g is additive )
let g be Function of (REAL-NS m),(REAL-NS n); :: thesis: ( f = g implies ( f is additive iff g is additive ) )
assume AS: f = g ; :: thesis: ( f is additive iff g is additive )

hereby :: thesis: ( g is additive implies f is additive )

assume AS1: f is additive ; :: thesis: g is additive

now

let x, y be Point of (REAL-NS m); :: thesis: g . (x + y) = (g . x) + (g . y)
reconsider x1 = x, y1 = y as Element of REAL m by REAL_NS1:def 4;
g . (x + y) = f . (x1 + y1) by AS, REAL_NS1:2
.= (f . x1) + (f . y1) by AS1, LOPBDef5 ;
hence g . (x + y) = (g . x) + (g . y) by AS, REAL_NS1:2; :: thesis: verum

end;

hence g is additive by GRCAT_1:def 13; :: thesis: verum

end;

assume AS1: g is additive ; :: thesis: f is additive

now

let x, y be Element of REAL m; :: thesis: f . (x + y) = (f . x) + (f . y)
reconsider x1 = x, y1 = y as Point of (REAL-NS m) by REAL_NS1:def 4;
f . (x + y) = g . (x1 + y1) by AS, REAL_NS1:2
.= (g . x1) + (g . y1) by AS1, GRCAT_1:def 13 ;
hence f . (x + y) = (f . x) + (f . y) by AS, REAL_NS1:2; :: thesis: verum

end;

hence f is additive by LOPBDef5; :: thesis: verum