let m, n be Element of NAT ; :: thesis: for f1, f2 being Function of (REAL m),(REAL n)
for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (REAL-NS m),(REAL-NS n)) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
let f1, f2 be Function of (REAL m),(REAL n); :: thesis: for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (REAL-NS m),(REAL-NS n)) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
let g1, g2 be Point of (R_NormSpace_of_BoundedLinearOperators (REAL-NS m),(REAL-NS n)); :: thesis: ( f1 = g1 & f2 = g2 implies f1 + f2 = g1 + g2 )
assume AS: ( f1 = g1 & f2 = g2 ) ; :: thesis: f1 + f2 = g1 + g2
set RB = R_NormSpace_of_BoundedLinearOperators (REAL-NS m),(REAL-NS n);
P0: ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then reconsider g12 = g1 + g2 as Function of (REAL m),(REAL n) by LOPBAN_1:def 10;
( g1 is LinearOperator of (REAL-NS m),(REAL-NS n) & g2 is LinearOperator of (REAL-NS m),(REAL-NS n) ) by LOPBAN_1:def 10;
then ( dom g1 = REAL m & dom g2 = REAL m ) by P0, FUNCT_2:def 1;
then P1: (dom f1) /\ (dom f2) = dom g12 by AS, FUNCT_2:def 1;
for c being Element of REAL m st c in dom g12 holds
g12 /. c = (f1 /. c) + (f2 /. c)

proof

let c be Element of REAL m; :: thesis: ( c in dom g12 implies g12 /. c = (f1 /. c) + (f2 /. c) )
assume c in dom g12 ; :: thesis: g12 /. c = (f1 /. c) + (f2 /. c)
reconsider x = c as VECTOR of (REAL-NS m) by REAL_NS1:def 4;
g12 /. c = (g1 . x) + (g2 . x) by LOPBAN_1:41;
hence g12 /. c = (f1 /. c) + (f2 /. c) by AS, REAL_NS1:2; :: thesis: verum

end;

hence f1 + f2 = g1 + g2 by P1, INTEGR15:def 9; :: thesis: verum