let m, n be Element of NAT ; :: thesis: for f1, f2 being PartFunc of (REAL m),(REAL n)
for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
let f1, f2 be PartFunc of (REAL m),(REAL n); :: thesis: for g1, g2 being PartFunc of (REAL-NS m),(REAL-NS n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
let g1, g2 be PartFunc of (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
( 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 PartFunc of (REAL m),(REAL n) ;
P1: (dom f1) /\ (dom f2) = dom g12 by AS, VFUNCT_1: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)
then P21: c in dom (g1 + g2) ;
P22: ( f1 /. c = g1 /. c & f2 /. c = g2 /. c ) by AS, REAL_NS1:def 4;
g12 /. c = (g1 + g2) /. c by REAL_NS1:def 4;
then g12 /. c = (g1 /. c) + (g2 /. c) by P21, VFUNCT_1:def 1;
hence g12 /. c = (f1 /. c) + (f2 /. c) by P22, REAL_NS1:2; :: thesis: verum

end;

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