let c be complex number ; :: 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 Lm4;
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:71, SEQ_4:68, SETWOP_2:41
.= c * (Sum F1) by Lm3
.= c * (Sum F) ; :: thesis: verum