let n, m be 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 A1: f = g ; :: thesis: ( f is additive iff g is additive )

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

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

now :: thesis: for x, y being Point of (REAL-NS m) holds g . (x + y) = (g . x) + (g . y)

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 A1, REAL_NS1:2
.= (f . x1) + (f . y1) by A2 ;
hence g . (x + y) = (g . x) + (g . y) by A1, REAL_NS1:2; :: thesis: verum

end;

hence g is additive by VECTSP_1:def 20; :: thesis: verum

end;

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

now :: thesis: for x, y being Element of REAL m holds f . (x + y) = (f . x) + (f . y)

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 A1, REAL_NS1:2
.= (g . x1) + (g . y1) by A3, VECTSP_1:def 20 ;
hence f . (x + y) = (f . x) + (f . y) by A1, REAL_NS1:2; :: thesis: verum

end;

hence f is additive ; :: thesis: verum