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

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