R is i -element FinSequence of COMPLEX by FINSEQ_1:102;
hence - R is Element of i -tuples_on COMPLEX by FINSEQ_2:113; :: thesis: verum