let n be Element of NAT ; :: thesis: for f1, f2 being PartFunc of REAL, the carrier of (REAL-NS n)
for g1, g2 being PartFunc of REAL,(REAL n) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
let f1, f2 be PartFunc of REAL, the carrier of (REAL-NS n); :: thesis: for g1, g2 being PartFunc of REAL,(REAL n) st f1 = g1 & f2 = g2 holds
f1 - f2 = g1 - g2
let g1, g2 be PartFunc of REAL,(REAL n); :: thesis: ( f1 = g1 & f2 = g2 implies f1 - f2 = g1 - g2 )
assume AS: ( f1 = g1 & f2 = g2 ) ; :: thesis: f1 - f2 = g1 - g2
K: dom (f1 - f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def 2;
then A2: dom (f1 - f2) = dom (g1 - g2) by AS, VALUED_2:def 46;

B1: now

let x be Element of REAL ; :: thesis: ( x in dom (f1 - f2) implies (f1 - f2) . x = (g1 - g2) . x )
assume A3: x in dom (f1 - f2) ; :: thesis: (f1 - f2) . x = (g1 - g2) . x
a: ( f1 /. x = g1 /. x & f2 /. x = g2 /. x ) by AS, REAL_NS1:def 4;
( x in dom f1 & x in dom f2 ) by A3, K, XBOOLE_0:def 4;
then ( g1 . x = g1 /. x & g2 /. x = g2 . x ) by AS, PARTFUN1:def 6;
then A5: (f1 /. x) - (f2 /. x) = (g1 . x) - (g2 . x) by a, REAL_NS1:5;
A6: (f1 - f2) /. x = (f1 /. x) - (f2 /. x) by A3, VFUNCT_1:def 2;
(f1 - f2) /. x = (f1 - f2) . x by A3, PARTFUN1:def 6;
hence (f1 - f2) . x = (g1 - g2) . x by A5, A6, A2, A3, VALUED_2:def 46; :: thesis: verum

end;

f1 - f2 is PartFunc of REAL,(REAL n) by REAL_NS1:def 4;
hence f1 - f2 = g1 - g2 by A2, B1, PARTFUN1:5; :: thesis: verum