( R1 is i -element FinSequence of COMPLEX & R2 is i -element FinSequence of COMPLEX ) by FINSEQ_1:102;
hence mlt (R1,R2) is Element of i -tuples_on COMPLEX by FINSEQ_2:120; :: thesis: verum