let c be Complex; :: thesis: for F being complex-valued FinSequence holds Sum (c * F) = c * (Sum F)
let F be complex-valued FinSequence; :: thesis: Sum (c * F) = c * (Sum F)
reconsider F1 = F as FinSequence of COMPLEX by Lm2;
reconsider s = c as Element of COMPLEX by XCMPLX_0:def 2;
set cM = multcomplex [;] (s,(id COMPLEX));
thus Sum (c * F) = (multcomplex [;] (s,(id COMPLEX))) . (addcomplex $$ F1) by SEQ_4:51, SEQ_4:54, SETWOP_2:30
.= c * (Sum F1) by Lm1
.= c * (Sum F) ; :: thesis: verum