let n, m be 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 A1: ( f1 = g1 & f2 = g2 ) ; :: thesis: f1 + f2 = g1 + g2
A2: ( 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 9;
( g1 is LinearOperator of (REAL-NS m),(REAL-NS n) & g2 is LinearOperator of (REAL-NS m),(REAL-NS n) ) by LOPBAN_1:def 9;
then ( dom g1 = REAL m & dom g2 = REAL m ) by A2, FUNCT_2:def 1;
then A3: (dom f1) /\ (dom f2) = dom g12 by A1, FUNCT_2:def 1;
A4: f1 <++> f2 = f1 + f2 by INTEGR15:def 9;
for c being object st c in dom g12 holds
g12 . c = (f1 . c) + (f2 . c)

proof

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

end;

hence f1 + f2 = g1 + g2 by A3, A4, VALUED_2:def 45; :: thesis: verum