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