let m be Element of NAT ; :: thesis: for f1, f2 being PartFunc of REAL,(REAL m) holds f1 - f2 = f1 + (- f2)
let f1, f2 be PartFunc of REAL,(REAL m); :: thesis: f1 - f2 = f1 + (- f2)
A1: dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_2:def 46;
A2: dom (f1 + (- f2)) = (dom f1) /\ (dom (- f2)) by VALUED_2:def 45;
A3: dom (- f2) = dom f2 by NFCONT_4:def 3;
now :: thesis: for x being object st x in dom (f1 - f2) holds
(f1 - f2) . x = (f1 + (- f2)) . x
let x be object ; :: thesis: ( x in dom (f1 - f2) implies (f1 - f2) . x = (f1 + (- f2)) . x )
assume A4: x in dom (f1 - f2) ; :: thesis: (f1 - f2) . x = (f1 + (- f2)) . x
then A5: x in dom f2 by A1, XBOOLE_0:def 4;
then A6: ( f2 . x = f2 /. x & (- f2) . x = (- f2) /. x ) by A3, PARTFUN1:def 6;
thus (f1 - f2) . x = (f1 . x) - (f2 . x) by A4, VALUED_2:def 46
.= (f1 . x) + ((- f2) . x) by A3, A5, A6, NFCONT_4:def 3
.= (f1 + (- f2)) . x by A1, A2, A3, A4, VALUED_2:def 45 ; :: thesis: verum
end;
hence f1 - f2 = f1 + (- f2) by A1, A2, A3, FUNCT_1:2; :: thesis: verum