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 A1: ( 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) ;
A2: (dom f1) /\ (dom f2) = dom g12 by A1, VFUNCT_1:def 2;
A5: f1 <--> f2 = f1 - f2 by INTEGR15:def 10;
for c being set st c in dom g12 holds
(g1 - g2) . c = (f1 . c) - (f2 . c)

proof

let c be set ; :: thesis: ( c in dom g12 implies (g1 - g2) . c = (f1 . c) - (f2 . c) )
assume A3: c in dom g12 ; :: thesis: (g1 - g2) . c = (f1 . c) - (f2 . c)
then A6: c in dom (g1 - g2) ;
( c in dom f1 & c in dom f2 ) by A2, A3, XBOOLE_0:def 4;
then A8: ( f1 /. c = f1 . c & f2 /. c = f2 . c ) by PARTFUN1:def 6;
A4: ( f1 /. c = g1 /. c & f2 /. c = g2 /. c ) by A1, REAL_NS1:def 4;
g12 . c = (g1 - g2) /. c by A3, PARTFUN1:def 6
.= (g1 /. c) - (g2 /. c) by A6, VFUNCT_1:def 2 ;
hence (g1 - g2) . c = (f1 . c) - (f2 . c) by A8, A4, REAL_NS1:5; :: thesis: verum

end;

hence f1 - f2 = g1 - g2 by A2, A5, VALUED_2:def 46; :: thesis: verum