R1 + R2 = addcomplex .: (R1,R2) by SEQ_4:def 6;
hence R1 + R2 is Element of i -tuples_on COMPLEX by FINSEQ_2:120; :: thesis: verum