A1: dom ((NAT --> 0) +* f) = (dom (NAT --> 0)) \/ (dom f) by FUNCT_4:def 1
.= NAT \/ (dom f)
.= NAT ;
for n being set st n in dom ((NAT --> 0) +* f) holds
((NAT --> 0) +* f) . n is Element of COMPLEX by XCMPLX_0:def 2;
hence (NAT --> 0) +* f is Complex_Sequence by A1, COMSEQ_1:1; :: thesis: verum