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);

now

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 A1: len F = 0 ; :: thesis: x * (Sum F) = Sum (x * F)
then F = <*> the carrier of L by FINSEQ_1:32;
then Sum F = 0. L by RLVECT_1:60;
then A2: x * (Sum F) = 0. L by VECTSP_1:36;
Seg (len (x * F)) = dom (x * F) by FINSEQ_1:def 3
.= dom F by POLYNOM1:def 2
.= Seg (len F) by FINSEQ_1:def 3 ;
then len (x * F) = 0 by A1;
then x * F = <*> the carrier of L by FINSEQ_1:32;
hence x * (Sum F) = Sum (x * F) by A2, RLVECT_1:60; :: thesis: verum

end;

then A3: S₁[ 0 ] ;

A4: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]

now

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) )
assume A6: len F = k + 1 ; :: thesis: x * (Sum F) = Sum (x * F)
set G = F | (Seg k);
reconsider G = F | (Seg k) as FinSequence by FINSEQ_1:19;
reconsider G = G as FinSequence of L by A6, Lm1;
A7: len G = k by A6, Lm1;
A8: F = G ^ <*(F /. (k + 1))*> by A6, Lm1;
thus x * (Sum F) = x * (Sum (G ^ <*(F /. (k + 1))*>)) by A6, Lm1
.= x * ((Sum G) + (Sum <*(F /. (k + 1))*>)) by RLVECT_1:58
.= (x * (Sum G)) + (x * (Sum <*(F /. (k + 1))*>)) by VECTSP_1:def 11
.= (Sum (x * G)) + (x * (Sum <*(F /. (k + 1))*>)) by A5, A7
.= (Sum (x * G)) + (x * (F /. (k + 1))) by RLVECT_1:61
.= (Sum (x * G)) + (Sum <*(x * (F /. (k + 1)))*>) by RLVECT_1:61
.= (Sum (x * G)) + (Sum (x * <*(F /. (k + 1))*>)) by POLYNOM1:21
.= Sum ((x * G) ^ (x * <*(F /. (k + 1))*>)) by RLVECT_1:58
.= Sum (x * F) by A8, POLYNOM1:23 ; :: thesis: verum

end;

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

end;

A9: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A4);
consider n being Element of NAT such that
A10: len F = n ;
thus x * (Sum F) = Sum (x * F) by A9, A10; :: thesis: verum