let L be non degenerated comRing; :: thesis: for F being non empty FinSequence of the carrier of (Polynom-Ring L)
for x being Element of L holds eval ((~ (Product F)),x) = Product (eval (F,x))
let F be non empty FinSequence of (Polynom-Ring L); :: thesis: for x being Element of L holds eval ((~ (Product F)),x) = Product (eval (F,x))
let x be Element of L; :: thesis: eval ((~ (Product F)),x) = Product (eval (F,x))
for k being non zero Nat st len F = k holds
eval ((~ (Product F)),x) = Product (eval (F,x))

proof

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

proof

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

proof

let F be FinSequence of the carrier of (Polynom-Ring L); :: thesis: ( len F = 1 implies eval ((~ (Product F)),x) = Product (eval (F,x)) )
assume A2: len F = 1 ; :: thesis: eval ((~ (Product F)),x) = Product (eval (F,x))
then dom F = Seg 1 by FINSEQ_1:def 3;
then A3: 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 A2, FINSEQ_1:40;
then A4: Product F = F . 1 by GROUP_4:9
.= F /. 1 by A3, PARTFUN1:def 6 ;
A5: dom (eval (F,x)) = dom F by Def8
.= Seg 1 by A2, FINSEQ_1:def 3 ;
set o1 = (eval (F,x)) . 1;
set o = (eval (F,x)) /. 1;
A6: 1 in dom (eval (F,x)) by A5;
A7: dom (eval (F,x)) = dom F by Def8;
eval (F,x) = <*((eval (F,x)) . 1)*> by A5, FINSEQ_1:def 8
.= <*((eval (F,x)) /. 1)*> by A6, PARTFUN1:def 6 ;
then Product (eval (F,x)) = (eval (F,x)) . 1 by GROUP_4:9
.= eval ((~ (Product F)),x) by A4, A6, A7, Def8 ;
hence eval ((~ (Product F)),x) = Product (eval (F,x)) ; :: thesis: verum

end;

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

end;

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

proof

let F be FinSequence of the carrier of (Polynom-Ring L); :: thesis: ( len F = k + 1 implies eval ((~ (Product F)),x) = Product (eval (F,x)) )
assume A10: len F = k + 1 ; :: thesis: eval ((~ (Product F)),x) = Product (eval (F,x))
then consider G being FinSequence of (Polynom-Ring L), d being Element of (Polynom-Ring L) such that
A11: F = G ^ <*d*> by FINSEQ_2:19;
(F | k) ^ <*(F /. (len F))*> = G ^ <*d*> by A11, A10, FINSEQ_5:21;
then A12: ( G = F | k & d = F /. (len F) ) by FINSEQ_2:17;
A13: k + 1 = (len G) + 1 by FINSEQ_2:16, A11, A10;
Product F = (Product G) * d by A11, GROUP_4:6;
then eval ((~ (Product F)),x) = (eval ((~ (Product G)),x)) * (eval ((~ d),x)) by Lm37
.= (Product (eval ((F | k),x))) * (eval ((~ (F /. (len F))),x)) by A13, A9, A12
.= Product ((eval ((F | k),x)) ^ <*(eval ((~ (F /. (len F))),x))*>) by GROUP_4:6
.= Product (eval (F,x)) by A10, Th25 ;
hence eval ((~ (Product F)),x) = Product (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(A1, A8);
hence ( len F = k implies eval ((~ (Product F)),x) = Product (eval (F,x)) ) ; :: thesis: verum

end;

hence eval ((~ (Product F)),x) = Product (eval (F,x)) ; :: thesis: verum