let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for F being FinSequence of the carrier of (Polynom-Ring (n,L))
for x being Function of n,L holds E_eval ((Sum F),x) = Sum (E_eval (F,x))
let L be non empty non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for F being FinSequence of the carrier of (Polynom-Ring (n,L))
for x being Function of n,L holds E_eval ((Sum F),x) = Sum (E_eval (F,x))
let F be FinSequence of the carrier of (Polynom-Ring (n,L)); :: thesis: for x being Function of n,L holds E_eval ((Sum F),x) = Sum (E_eval (F,x))
let x be Function of n,L; :: thesis: E_eval ((Sum F),x) = Sum (E_eval (F,x))

per cases ( len F = 0 or len F <> 0 ) ;

suppose A1: len F = 0 ; :: thesis: E_eval ((Sum F),x) = Sum (E_eval (F,x))

then A2: F = <*> the carrier of (Polynom-Ring (n,L)) ;
A3: 0. (Polynom-Ring (n,L)) = 0_ (n,L) by POLYNOM1:def 11;
A4: E_eval ((Sum F),x) = E_eval ((0. (Polynom-Ring (n,L))),x) by A2, RLVECT_1:43
.= eval ((0_ (n,L)),x) by A3, Def1
.= 0. L by POLYNOM2:20 ;
Seg (len F) = dom F by FINSEQ_1:def 3
.= dom (E_eval (F,x)) by Def2
.= Seg (len (E_eval (F,x))) by FINSEQ_1:def 3 ;
then E_eval (F,x) = <*> the carrier of L by A1;
hence E_eval ((Sum F),x) = Sum (E_eval (F,x)) by A4, RLVECT_1:43; :: thesis: verum

end;

suppose A5: len F <> 0 ; :: thesis: E_eval ((Sum F),x) = Sum (E_eval (F,x))

for k being non zero Nat st len F = k holds
E_eval ((Sum F),x) = Sum (E_eval (F,x))

proof

let k be non zero Nat; :: thesis: ( len F = k implies E_eval ((Sum F),x) = Sum (E_eval (F,x)) )
defpred S₁[ Nat] means for F being FinSequence of the carrier of (Polynom-Ring (n,L)) st len F = $1 holds
E_eval ((Sum F),x) = Sum (E_eval (F,x));
A6: S₁[1]

proof

for F being FinSequence of the carrier of (Polynom-Ring (n,L)) st len F = 1 holds
E_eval ((Sum F),x) = Sum (E_eval (F,x))

proof

let F be FinSequence of the carrier of (Polynom-Ring (n,L)); :: thesis: ( len F = 1 implies E_eval ((Sum F),x) = Sum (E_eval (F,x)) )
assume A7: len F = 1 ; :: thesis: E_eval ((Sum F),x) = Sum (E_eval (F,x))
then dom F = Seg 1 by FINSEQ_1:def 3;
then A9: 1 in dom F ;
then F . 1 in rng F by FUNCT_1:3;
then reconsider o = F . 1 as Element of (Polynom-Ring (n,L)) ;
F = <*o*> by A7, FINSEQ_1:40;
then A11: Sum F = F . 1 by BINOM:3
.= F /. 1 by A9, PARTFUN1:def 6 ;
A12: dom (E_eval (F,x)) = dom F by Def2
.= Seg 1 by A7, FINSEQ_1:def 3 ;
set o1 = (E_eval (F,x)) . 1;
set o = (E_eval (F,x)) /. 1;
A13: 1 in dom (E_eval (F,x)) by A12;
A14: dom (E_eval (F,x)) = dom F by Def2;
E_eval (F,x) = <*((E_eval (F,x)) . 1)*> by A12, FINSEQ_1:def 8
.= <*((E_eval (F,x)) /. 1)*> by A13, PARTFUN1:def 6 ;
then Sum (E_eval (F,x)) = (E_eval (F,x)) . 1 by BINOM:3
.= E_eval ((Sum F),x) by A11, A13, A14, Def2 ;
hence E_eval ((Sum F),x) = Sum (E_eval (F,x)) ; :: thesis: verum

end;

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

end;

A15: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A16: S₁[k] ; :: thesis: S₁[k + 1]
for F being FinSequence of the carrier of (Polynom-Ring (n,L)) st len F = k + 1 holds
E_eval ((Sum F),x) = Sum (E_eval (F,x))

proof

let F be FinSequence of the carrier of (Polynom-Ring (n,L)); :: thesis: ( len F = k + 1 implies E_eval ((Sum F),x) = Sum (E_eval (F,x)) )
assume A17: len F = k + 1 ; :: thesis: E_eval ((Sum F),x) = Sum (E_eval (F,x))
then consider G being FinSequence of (Polynom-Ring (n,L)), d being Element of (Polynom-Ring (n,L)) such that
A18: F = G ^ <*d*> by FINSEQ_2:19;
(F | k) ^ <*(F /. (len F))*> = G ^ <*d*> by A18, A17, FINSEQ_5:21;
then A20: ( G = F | k & d = F /. (len F) ) by FINSEQ_2:17;
A21: k + 1 = (len G) + 1 by FINSEQ_2:16, A18, A17;
Sum F = (Sum G) + d by A18, FVSUM_1:71;
then E_eval ((Sum F),x) = (E_eval ((Sum G),x)) + (E_eval (d,x)) by Th2
.= (Sum (E_eval ((F | k),x))) + (E_eval ((F /. (len F)),x)) by A21, A16, A20
.= Sum ((E_eval ((F | k),x)) ^ <*(E_eval ((F /. (len F)),x))*>) by FVSUM_1:71
.= Sum (E_eval (F,x)) by A17, Th4 ;
hence E_eval ((Sum F),x) = Sum (E_eval (F,x)) ; :: thesis: verum

end;

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

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A6, A15);
hence ( len F = k implies E_eval ((Sum F),x) = Sum (E_eval (F,x)) ) ; :: thesis: verum

end;

hence E_eval ((Sum F),x) = Sum (E_eval (F,x)) by A5; :: thesis: verum

end;

end;