let L be Field; :: thesis: for f being FinSequence of (Polynom-Ring L) st ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) holds
for p being Polynomial of L st p = Product f holds
for x being Element of L holds
( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
let f be FinSequence of (Polynom-Ring L); :: thesis: ( ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds
for x being Element of L holds
( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) ) )
assume A1: for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ; :: thesis: for p being Polynomial of L st p = Product f holds
for x being Element of L holds
( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
let p be Polynomial of L; :: thesis: ( p = Product f implies for x being Element of L holds
( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) ) )
assume A2: p = Product f ; :: thesis: for x being Element of L holds
( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
let x be Element of L; :: thesis: ( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )

A3: now :: thesis: ( ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) implies eval (p,x) = 0. L )

assume ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) ; :: thesis: eval (p,x) = 0. L
then consider i being Nat such that
A4: ( i in dom f & f . i = rpoly (1,x) ) ;
reconsider g = Del (f,i) as FinSequence of (Polynom-Ring L) ;
reconsider q = Product g as Polynomial of L by POLYNOM3:def 10;
A5: f /. i = rpoly (1,x) by A4, PARTFUN1:def 6;
Product f = (f /. i) * (Product g) by A4, Th3;
then p = (rpoly (1,x)) *' q by A2, A5, POLYNOM3:def 10;
then A6: eval (p,x) = (eval ((rpoly (1,x)),x)) * (eval (q,x)) by POLYNOM4:24;
eval ((rpoly (1,x)),x) = x - x by HURWITZ:29
.= 0. L by RLVECT_1:15 ;
hence eval (p,x) = 0. L by A6; :: thesis: verum

end;

now :: thesis: ( eval (p,x) = 0. L implies ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )

assume A7: eval (p,x) = 0. L ; :: thesis: ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
defpred S₁[ Nat] means for f being FinSequence of (Polynom-Ring L) st len f = $1 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) holds
for p being Polynomial of L st p = Product f holds
for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) );

now :: thesis: for f being FinSequence of (Polynom-Ring L) st len f = 0 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) holds
for p being Polynomial of L st p = Product f holds
for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )

let f be FinSequence of (Polynom-Ring L); :: thesis: ( len f = 0 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds
for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
assume A8: ( len f = 0 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) ) ; :: thesis: for p being Polynomial of L st p = Product f holds
for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
let p be Polynomial of L; :: thesis: ( p = Product f implies for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
assume A9: p = Product f ; :: thesis: for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
let x be Element of L; :: thesis: ( eval (p,x) = 0. L implies ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
assume A10: eval (p,x) = 0. L ; :: thesis: ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
f = <*> the carrier of (Polynom-Ring L) by A8;
then p = 1_ (Polynom-Ring L) by A9, GROUP_4:8
.= 1_. L by POLYNOM3:def 10 ;
hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by A10, POLYNOM4:18; :: thesis: verum

end;

then A11: S₁[ 0 ] ;

A12: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

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

now :: thesis: for f being FinSequence of (Polynom-Ring L) st len f = n + 1 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) holds
for p being Polynomial of L st p = Product f holds
for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )

let f be FinSequence of (Polynom-Ring L); :: thesis: ( len f = n + 1 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds
for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
assume A14: ( len f = n + 1 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) ) ; :: thesis: for p being Polynomial of L st p = Product f holds
for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
let p be Polynomial of L; :: thesis: ( p = Product f implies for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
assume A15: p = Product f ; :: thesis: for x being Element of L st eval (p,x) = 0. L holds
ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
let x be Element of L; :: thesis: ( eval (p,x) = 0. L implies ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) )
assume A16: eval (p,x) = 0. L ; :: thesis: ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
f <> {} by A14;
then consider g being FinSequence, u being object such that
A17: f = g ^ <*u*> by FINSEQ_1:46;
reconsider g = g as FinSequence of (Polynom-Ring L) by A17, FINSEQ_1:36;
A18: dom f = Seg (n + 1) by A14, FINSEQ_1:def 3;
1 <= n + 1 by NAT_1:11;
then A19: n + 1 in dom f by A18;
A20: n + 1 = (len g) + (len <*u*>) by A14, A17, FINSEQ_1:22
.= (len g) + 1 by FINSEQ_1:40 ;
A21: f . (n + 1) = u by A20, A17, FINSEQ_1:42;
then consider z being Element of L such that
A22: u = rpoly (1,z) by A14, A19;
reconsider u = u as Element of (Polynom-Ring L) by A22, POLYNOM3:def 10;
reconsider q = Product g as Polynomial of L by POLYNOM3:def 10;
Product f = (Product g) * u by A17, GROUP_4:6
.= q *' (rpoly (1,z)) by A22, POLYNOM3:def 10 ;
then A23: eval (p,x) = (eval (q,x)) * (eval ((rpoly (1,z)),x)) by A15, POLYNOM4:24;

A24: now :: thesis: for i being Nat st i in dom g holds
ex z being Element of L st g . i = rpoly (1,z)

let i be Nat; :: thesis: ( i in dom g implies ex z being Element of L st g . i = rpoly (1,z) )
assume A25: i in dom g ; :: thesis: ex z being Element of L st g . i = rpoly (1,z)
A26: dom g c= dom f by A17, FINSEQ_1:26;
g . i = f . i by A25, A17, FINSEQ_1:def 7;
hence ex z being Element of L st g . i = rpoly (1,z) by A25, A26, A14; :: thesis: verum

end;

now :: thesis: ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )

per cases ( eval (q,x) = 0. L or eval ((rpoly (1,z)),x) = 0. L ) by A23, A16, VECTSP_2:def 1;

suppose eval (q,x) = 0. L ; :: thesis: ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )

then consider i being Nat such that
A27: ( i in dom g & g . i = rpoly (1,x) ) by A20, A24, A13;
A28: dom g c= dom f by A17, FINSEQ_1:26;
f . i = rpoly (1,x) by A27, A17, FINSEQ_1:def 7;
hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by A28, A27; :: thesis: verum

end;

suppose eval ((rpoly (1,z)),x) = 0. L ; :: thesis: ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )

then x - z = 0. L by HURWITZ:29;
then x = z by RLVECT_1:21;
hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by A19, A21, A22; :: thesis: verum

end;

end;

end;

hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) ; :: thesis: verum

end;

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

end;

A29: for n being Nat holds S₁[n] from NAT_1:sch 2(A11, A12);
len f is Nat ;
hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by A7, A1, A2, A29; :: thesis: verum

end;

hence ( eval (p,x) = 0. L iff ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) ) by A3; :: thesis: verum