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