reconsider q = r as Element of COMPLEX by XCMPLX_0:def 2;
q * R = (multcomplex [;] q,(id COMPLEX )) * R by Lm1;
hence r * R is Element of i -tuples_on COMPLEX by FINSEQ_2:133; :: thesis: verum