dom (seq * Nseq) = NAT by FUNCT_2:def 1;
hence Nseq (#) seq is Complex_Sequence ; :: thesis: verum