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:113; :: thesis: verum