let i be Nat; :: thesis: for c being complex number
for R being i -element FinSequence of COMPLEX holds mlt ((i |-> c),R) = c * R
let c be complex number ; :: thesis: for R being i -element FinSequence of COMPLEX holds mlt ((i |-> c),R) = c * R
let R be i -element FinSequence of COMPLEX ; :: thesis: mlt ((i |-> c),R) = c * R
reconsider s = c as Element of COMPLEX by XCMPLX_0:def 2;
mlt ((i |-> s),R) = multcomplex [;] (s,R) by FINSEQOP:20
.= c * R by FINSEQOP:22 ;
hence mlt ((i |-> c),R) = c * R ; :: thesis: verum