c in COMPLEX by XCMPLX_0:def 2;
hence NAT --> c is Complex_Sequence by FUNCOP_1:45; :: thesis: verum