let L be non empty right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for a being Element of L
for p being FinSequence of the carrier of L holds Sum (p * a) = (Sum p) * a
let a be Element of L; :: thesis: for p being FinSequence of the carrier of L holds Sum (p * a) = (Sum p) * a
set p = <*> the carrier of L;
defpred S₁[ FinSequence of the carrier of L] means Sum ($1 * a) = (Sum $1) * a;

A1: now :: thesis: for p being FinSequence of the carrier of L
for r being Element of L st S₁[p] holds
S₁[p ^ <*r*>]

let p be FinSequence of the carrier of L; :: thesis: for r being Element of L st S₁[p] holds
S₁[p ^ <*r*>]
let r be Element of L; :: thesis: ( S₁[p] implies S₁[p ^ <*r*>] )
assume A2: S₁[p] ; :: thesis: S₁[p ^ <*r*>]
Sum ((p ^ <*r*>) * a) = Sum ((p * a) ^ (<*r*> * a)) by Th11
.= (Sum (p * a)) + (Sum (<*r*> * a)) by RLVECT_1:41
.= (Sum (p * a)) + (Sum <*(r * a)*>) by Th9
.= (Sum (p * a)) + (r * a) by RLVECT_1:44
.= ((Sum p) * a) + ((Sum <*r*>) * a) by A2, RLVECT_1:44
.= ((Sum p) + (Sum <*r*>)) * a by VECTSP_1:def 7
.= (Sum (p ^ <*r*>)) * a by RLVECT_1:41 ;
hence S₁[p ^ <*r*>] ; :: thesis: verum

end;

( Sum (<*> the carrier of L) = 0. L & Sum ((<*> the carrier of L) * a) = Sum (<*> the carrier of L) ) by Th7, RLVECT_1:43;
then A3: S₁[ <*> the carrier of L] ;
thus for p being FinSequence of the carrier of L holds S₁[p] from FINSEQ_2:sch 2(A3, A1); :: thesis: verum