let L be comRing; :: thesis: for F being FinSequence of the carrier of (Polynom-Ring L)
for x being Element of L holds eval ((~ (Sum F)),x) = Sum (eval (F,x))
let F be FinSequence of the carrier of (Polynom-Ring L); :: thesis: for x being Element of L holds eval ((~ (Sum F)),x) = Sum (eval (F,x))
let x be Element of L; :: thesis: eval ((~ (Sum F)),x) = Sum (eval (F,x))

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

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

then A2: F = <*> the carrier of (Polynom-Ring L) ;
0. (Polynom-Ring L) = 0_. L by POLYNOM3:def 10;
then A4: eval ((~ (Sum F)),x) = eval ((0_. L),x) by A2, RLVECT_1:43
.= 0. L by POLYNOM4:17 ;
Seg (len F) = dom F by FINSEQ_1:def 3
.= dom (eval (F,x)) by Def8
.= Seg (len (eval (F,x))) by FINSEQ_1:def 3 ;
then eval (F,x) = <*> the carrier of L by A1;
hence eval ((~ (Sum F)),x) = Sum (eval (F,x)) by A4, RLVECT_1:43; :: thesis: verum

end;

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

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

proof

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

proof

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

proof

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

end;

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

end;

A13: 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 A14: S₁[k] ; :: thesis: S₁[k + 1]
for F being FinSequence of the carrier of (Polynom-Ring L) st len F = k + 1 holds
eval ((~ (Sum F)),x) = Sum (eval (F,x))

proof

let F be FinSequence of the carrier of (Polynom-Ring L); :: thesis: ( len F = k + 1 implies eval ((~ (Sum F)),x) = Sum (eval (F,x)) )
assume A15: len F = k + 1 ; :: thesis: eval ((~ (Sum F)),x) = Sum (eval (F,x))
then consider G being FinSequence of (Polynom-Ring L), d being Element of (Polynom-Ring L) such that
A16: F = G ^ <*d*> by FINSEQ_2:19;
(F | k) ^ <*(F /. (len F))*> = G ^ <*d*> by A16, A15, FINSEQ_5:21;
then A17: ( G = F | k & d = F /. (len F) ) by FINSEQ_2:17;
A18: k + 1 = (len G) + 1 by FINSEQ_2:16, A16, A15;
Sum F = (Sum G) + d by A16, FVSUM_1:71;
then eval ((~ (Sum F)),x) = (eval ((~ (Sum G)),x)) + (eval ((~ d),x)) by Lm15
.= (Sum (eval ((F | k),x))) + (eval ((~ (F /. (len F))),x)) by A18, A14, A17
.= Sum ((eval ((F | k),x)) ^ <*(eval ((~ (F /. (len F))),x))*>) by FVSUM_1:71
.= Sum (eval (F,x)) by A15, Th25 ;
hence eval ((~ (Sum F)),x) = Sum (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, A13);
hence ( len F = k implies eval ((~ (Sum F)),x) = Sum (eval (F,x)) ) ; :: thesis: verum

end;

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

end;

end;