A1: dom (f + f1) = (dom f) /\ (dom f1) by VALUED_1:def 1
.= dom f by PARTFUN1:def 2 ;
reconsider f1 = f1 as complex-valued Function ;
for k being object st k in dom f holds
(f + f1) . k = f . k

proof

let k be object ; :: thesis: ( k in dom f implies (f + f1) . k = f . k )
assume B1: k in dom f ; :: thesis: (f + f1) . k = f . k
(f + f1) . k = (f . k) + (f1 . k) by A1, B1, VALUED_1:def 1
.= (f . k) + 0 ;
hence (f + f1) . k = f . k ; :: thesis: verum

end;

hence f + f1 = f by A1, FUNCT_1:2; :: thesis: verum