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