R1 + R2 = addcomplex .: R1,R2 by COMPLSP1:def 7;
hence R1 + R2 is Element of i -tuples_on COMPLEX by FINSEQ_2:140; :: thesis: verum