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