( dom (NAT --> 0) = NAT & ( for x being set st x in NAT holds
(NAT --> 0) . x is Element of COMPLEX ) ) by XCMPLX_0:def 2;
then reconsider cseq = NAT --> 0 as Complex_Sequence by COMSEQ_1:1;
for n being Nat holds cseq . n = 0 ;
hence Partial_Sums (NAT --> 0) = NAT --> 0 by PARTFUN1:def 2, COMSEQ_3:24; :: thesis: verum