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) ) )
thus A1: dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def 1; :: thesis: for c being Element of C st c in dom (f1 + f2) holds
(f1 + f2) /. c = (f1 /. c) + (f2 /. c)

now

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 ( c in dom f1 & c in dom f2 ) by A1, XBOOLE_0:def 4;
then A3: ( f1 . c = f1 /. c & f2 . c = f2 /. c ) by PARTFUN1:def 8;
thus (f1 + f2) /. c = (f1 + f2) . c by A2, PARTFUN1:def 8
.= (f1 /. c) + (f2 /. c) by A2, A3, VALUED_1:def 1 ; :: 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