let n be Element of NAT ; :: thesis: for W being non empty set
for f1, f2 being PartFunc of W,(REAL-NS n)
for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
let W be non empty set ; :: thesis: for f1, f2 being PartFunc of W,(REAL-NS n)
for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
let f1, f2 be PartFunc of W,(REAL-NS n); :: thesis: for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds
f1 + f2 = g1 + g2
let g1, g2 be PartFunc of W,(REAL n); :: thesis: ( f1 = g1 & f2 = g2 implies f1 + f2 = g1 + g2 )
assume A1: ( f1 = g1 & f2 = g2 ) ; :: thesis: f1 + f2 = g1 + g2
A2: dom (f1 + f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def 1;
then A3: dom (f1 + f2) = dom (g1 + g2) by A1, VALUED_2:def 45;

A4: now :: thesis: for x being Element of W st x in dom (f1 + f2) holds
(f1 + f2) . x = (g1 + g2) . x

let x be Element of W; :: thesis: ( x in dom (f1 + f2) implies (f1 + f2) . x = (g1 + g2) . x )
assume A5: x in dom (f1 + f2) ; :: thesis: (f1 + f2) . x = (g1 + g2) . x
then A6: ( x in dom g1 & x in dom g2 ) by A2, A1, XBOOLE_0:def 4;
A7: ( f1 /. x = g1 /. x & f2 /. x = g2 /. x ) by A1, REAL_NS1:def 4;
( g1 /. x = g1 . x & g2 /. x = g2 . x ) by A6, PARTFUN1:def 6;
then A8: (f1 /. x) + (f2 /. x) = (g1 . x) + (g2 . x) by A7, REAL_NS1:2;
(f1 + f2) /. x = (f1 /. x) + (f2 /. x) by A5, VFUNCT_1:def 1;
then (f1 + f2) . x = (f1 /. x) + (f2 /. x) by A5, PARTFUN1:def 6;
hence (f1 + f2) . x = (g1 + g2) . x by A8, A3, A5, VALUED_2:def 45; :: thesis: verum

end;

f1 + f2 is PartFunc of W,(REAL n) by REAL_NS1:def 4;
hence f1 + f2 = g1 + g2 by A3, A4, PARTFUN1:5; :: thesis: verum