let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for x being Element of L
for F being FinSequence of L holds x * (Sum F) = Sum (x * F)
let x be Element of L; :: thesis: for F being FinSequence of L holds x * (Sum F) = Sum (x * F)
let F be FinSequence of L; :: thesis: x * (Sum F) = Sum (x * F)
defpred S₁[ Nat] means for x being Element of L
for F being FinSequence of L st len F = $1 holds
x * (Sum F) = Sum (x * F);
A1: ex n being Element of NAT st len F = n ;

A2: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for x being Element of L
for F being FinSequence of L st len F = k + 1 holds
x * (Sum F) = Sum (x * F)

let x be Element of L; :: thesis: for F being FinSequence of L st len F = k + 1 holds
x * (Sum F) = Sum (x * F)
let F be FinSequence of L; :: thesis: ( len F = k + 1 implies x * (Sum F) = Sum (x * F) )
set G = F | (Seg k);
reconsider G = F | (Seg k) as FinSequence by FINSEQ_1:15;
assume A4: len F = k + 1 ; :: thesis: x * (Sum F) = Sum (x * F)
then reconsider G = G as FinSequence of L by Lm1;
A5: len G = k by A4, Lm1;
A6: F = G ^ <*(F /. (k + 1))*> by A4, Lm1;
thus x * (Sum F) = x * (Sum (G ^ <*(F /. (k + 1))*>)) by A4, Lm1
.= x * ((Sum G) + (Sum <*(F /. (k + 1))*>)) by RLVECT_1:41
.= (x * (Sum G)) + (x * (Sum <*(F /. (k + 1))*>)) by VECTSP_1:def 2
.= (Sum (x * G)) + (x * (Sum <*(F /. (k + 1))*>)) by A3, A5
.= (Sum (x * G)) + (x * (F /. (k + 1))) by RLVECT_1:44
.= (Sum (x * G)) + (Sum <*(x * (F /. (k + 1)))*>) by RLVECT_1:44
.= (Sum (x * G)) + (Sum (x * <*(F /. (k + 1))*>)) by POLYNOM1:8
.= Sum ((x * G) ^ (x * <*(F /. (k + 1))*>)) by RLVECT_1:41
.= Sum (x * F) by A6, POLYNOM1:10 ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

now :: thesis: for x being Element of L
for F being FinSequence of L st len F = 0 holds
x * (Sum F) = Sum (x * F)

let x be Element of L; :: thesis: for F being FinSequence of L st len F = 0 holds
x * (Sum F) = Sum (x * F)
let F be FinSequence of L; :: thesis: ( len F = 0 implies x * (Sum F) = Sum (x * F) )
assume A7: len F = 0 ; :: thesis: x * (Sum F) = Sum (x * F)
Seg (len (x * F)) = dom (x * F) by FINSEQ_1:def 3
.= dom F by POLYNOM1:def 1
.= Seg (len F) by FINSEQ_1:def 3 ;
then len (x * F) = 0 by A7;
then A8: x * F = <*> the carrier of L ;
F = <*> the carrier of L by A7;
then Sum F = 0. L by RLVECT_1:43;
then x * (Sum F) = 0. L ;
hence x * (Sum F) = Sum (x * F) by A8, RLVECT_1:43; :: thesis: verum

end;

then A9: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A2);
hence x * (Sum F) = Sum (x * F) by A1; :: thesis: verum