A1: dom (Partial_Sums s) = NAT by PARTFUN1:def 2;
rng (Partial_Sums s) c= COMPLEX by VALUED_0:def 1;
then Partial_Sums s is PartFunc of NAT,COMPLEX by A1, RELSET_1:4;
hence Partial_Sums s is Complex_Sequence ; :: thesis: verum