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

proof

let k be object ; :: thesis: ( k in dom f implies f . k = (f + g) . k )
assume A1: k in dom f ; :: thesis: f . k = (f + g) . k
reconsider c = f . k as Complex ;
g . k = 0 ;
then c = (f . k) + (g . k)
.= (f + g) . k by A0, A1, VALUED_1:def 1 ;
hence f . k = (f + g) . k ; :: thesis: verum

end;

hence f + g = f by A0, FUNCT_1:def 11; :: thesis: verum