let n be Element of NAT ; 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 ; 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); 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); ( f1 = g1 & f2 = g2 implies f1 - f2 = g1 - g2 )
assume A1:
( f1 = g1 & f2 = g2 )
; f1 - f2 = g1 - g2
A2:
dom (f1 - f2) = (dom f1) /\ (dom f2)
by VFUNCT_1:def 2;
then A3:
dom (f1 - f2) = dom (g1 - g2)
by A1, VALUED_2:def 46;
A4:
now for x being Element of W st x in dom (f1 - f2) holds
(f1 - f2) . x = (g1 - g2) . xlet x be
Element of
W;
( x in dom (f1 - f2) implies (f1 - f2) . x = (g1 - g2) . x )assume A5:
x in dom (f1 - f2)
;
(f1 - f2) . x = (g1 - g2) . xA6:
(
f1 /. x = g1 /. x &
f2 /. x = g2 /. x )
by A1, REAL_NS1:def 4;
(
x in dom f1 &
x in dom f2 )
by A5, A2, XBOOLE_0:def 4;
then
(
g1 . x = g1 /. x &
g2 /. x = g2 . x )
by A1, PARTFUN1:def 6;
then A7:
(f1 /. x) - (f2 /. x) = (g1 . x) - (g2 . x)
by A6, REAL_NS1:5;
A8:
(f1 - f2) /. x = (f1 /. x) - (f2 /. x)
by A5, VFUNCT_1:def 2;
(f1 - f2) /. x = (f1 - f2) . x
by A5, PARTFUN1:def 6;
hence
(f1 - f2) . x = (g1 - g2) . x
by A7, A8, A3, A5, VALUED_2:def 46;
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; verum