for C being non empty set
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) ) )