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);
( the addF of K is having_a_unity & the multF of K is_distributive_wrt the addF of K ) by Th10, Th12;
hence Sum (a * p) = (the multF of K [;] a,(id the carrier of K)) . (Sum p) by Th17, SETWOP_2:41
.= a * (Sum p) by Lm1 ;
:: thesis: verum