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 COMPLSP1:7, COMPLSP1:15, SETWOP_2:41
.= a * (Sum F) by Lm2 ; :: thesis: verum