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