let F be FinSequence of COMPLEX ; :: thesis: for a being Element of COMPLEX holds Sum (a * F) = a * (Sum F)
let a be Element of COMPLEX ; :: thesis: Sum (a * F) = a * (Sum F)
set rM = multcomplex [;] (a,(id COMPLEX));
thus Sum (a * F) = addcomplex $$ ((multcomplex [;] (a,(id COMPLEX))) * F) by Lm1
.= (multcomplex [;] (a,(id COMPLEX))) . (addcomplex $$ F) by SEQ_4:51, SEQ_4:54, SETWOP_2:30
.= a * (Sum F) by Lm2 ; :: thesis: verum