let C be non empty set ; :: thesis: for f1, f2 being PartFunc of C,COMPLEX holds
( dom (f1 - f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 - f2) holds
(f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) )
let f1, f2 be PartFunc of C,COMPLEX; :: thesis: ( dom (f1 - f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 - f2) holds
(f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) )
A1: dom (f1 - f2) = (dom f1) /\ (dom (- f2)) by VALUED_1:def 1;
hence dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_1:8; :: thesis: for c being Element of C st c in dom (f1 - f2) holds
(f1 - f2) /. c = (f1 /. c) - (f2 /. c)

now :: thesis: for c being Element of C st c in dom (f1 - f2) holds
(f1 - f2) /. c = (f1 /. c) - (f2 /. c)

let c be Element of C; :: thesis: ( c in dom (f1 - f2) implies (f1 - f2) /. c = (f1 /. c) - (f2 /. c) )
assume A2: c in dom (f1 - f2) ; :: thesis: (f1 - f2) /. c = (f1 /. c) - (f2 /. c)
then A3: ( dom (- f2) = dom f2 & c in dom (- f2) ) by A1, VALUED_1:8, XBOOLE_0:def 4;
c in dom f1 by A1, A2, XBOOLE_0:def 4;
then A4: f1 /. c = f1 . c by PARTFUN1:def 6;
thus (f1 - f2) /. c = (f1 - f2) . c by A2, PARTFUN1:def 6
.= (f1 . c) - (f2 . c) by A2, VALUED_1:13
.= (f1 /. c) - (f2 /. c) by A3, A4, PARTFUN1:def 6 ; :: thesis: verum

end;

hence for c being Element of C st c in dom (f1 - f2) holds
(f1 - f2) /. c = (f1 /. c) - (f2 /. c) ; :: thesis: verum