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 (a * p) = a * (Sum p)
let a be Element of L; :: thesis: for p being FinSequence of the carrier of L holds Sum (a * p) = a * (Sum p)
set p = <*> the carrier of L;
defpred S₁[ FinSequence of the carrier of L] means Sum (a * $1) = a * (Sum $1);

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 (a * (p ^ <*r*>)) = Sum ((a * p) ^ (a * <*r*>)) by Th10
.= (Sum (a * p)) + (Sum (a * <*r*>)) by RLVECT_1:41
.= (Sum (a * p)) + (Sum <*(a * r)*>) by Th8
.= (Sum (a * p)) + (a * r) by RLVECT_1:44
.= (a * (Sum p)) + (a * (Sum <*r*>)) by A2, RLVECT_1:44
.= a * ((Sum p) + (Sum <*r*>)) by VECTSP_1:def 7
.= a * (Sum (p ^ <*r*>)) by RLVECT_1:41 ;
hence S₁[p ^ <*r*>] ; :: thesis: verum

end;

( Sum (<*> the carrier of L) = 0. L & Sum (a * (<*> the carrier of L)) = Sum (<*> the carrier of L) ) by Th6, 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