let i be Nat; :: thesis: for c being complex number
for R being i -long FinSequence of COMPLEX holds mlt (i |-> c),R = c * R
let c be complex number ; :: thesis: for R being i -long FinSequence of COMPLEX holds mlt (i |-> c),R = c * R
let R be i -long 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:21
.= c * R by FINSEQOP:23 ;
hence mlt (i |-> c),R = c * R ; :: thesis: verum