let K be non empty right_complementable Abelian add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for a being Element of K
for p being FinSequence of the carrier of K holds Sum (a * p) = a * (Sum p)
let a be Element of K; :: thesis: for p being FinSequence of the carrier of K holds Sum (a * p) = a * (Sum p)
let p be FinSequence of the carrier of K; :: thesis: Sum (a * p) = a * (Sum p)
set rM = the multF of K [;] a,(id the carrier of K);
A1: ( the addF of K is commutative & the addF of K is associative & the addF of K is having_a_unity ) by Th10;
the multF of K is_distributive_wrt the addF of K by Th12;
hence Sum (a * p) = (the multF of K [;] a,(id the carrier of K)) . (Sum p) by A1, Th17, SETWOP_2:41
.= a * (Sum p) by Lm1 ;
:: thesis: verum