let K be non empty right_complementable distributive Abelian add-associative right_zeroed 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 Th8, Th10;
hence Sum (a * p) = ( the multF of K [;] (a,(id the carrier of K))) . (Sum p) by Th14, SETWOP_2:30
.= a * (Sum p) by Lm1 ;
:: thesis: verum