- R = compcomplex * R by SEQ_4:def 8;
hence - R is Element of i -tuples_on COMPLEX by FINSEQ_2:113; :: thesis: verum