let n, m be Nat; 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); 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); ( f1 = g1 & f2 = g2 implies f1 - f2 = g1 - g2 )
assume A1:
( f1 = g1 & f2 = g2 )
; 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;
A3:
f1 <--> f2 = f1 - f2
by INTEGR15:def 10;
for c being object st c in dom g12 holds
(g1 - g2) . c = (f1 . c) - (f2 . c)
hence
f1 - f2 = g1 - g2
by A2, A3, VALUED_2:def 46; verum