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 AS1: 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 AS2: 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) ) )

A: 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
A1: ( i in dom f & f . i = rpoly (1,x) ) ;
reconsider g = Del (f,i) as FinSequence of (Polynom-Ring L) by FINSEQ_3:105;
reconsider q = Product g as Polynomial of L by POLYNOM3:def 10;
A2: f /. i = rpoly (1,x) by A1, PARTFUN1:def 6;
Product f = (f /. i) * (Product g) by A1, del1;
then p = (rpoly (1,x)) *' q by AS2, A2, POLYNOM3:def 10;
then A3: 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 A3, VECTSP_1:7; :: 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 A0: 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 A1: ( 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 A2: 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 A3: 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 A1;
then p = 1_ (Polynom-Ring L) by A2, 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 A3, POLYNOM4:18; :: thesis: verum

end;

then IA: S₁[ 0 ] ;

IS: 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 IV: 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 A1: ( 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 A2: 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 A3: eval (p,x) = 0. L ; :: thesis: ex i being Nat st
( i in dom f & f . i = rpoly (1,x) )
f <> {} by A1;
then consider g being FinSequence, u being set such that
A6: f = g ^ <*u*> by FINSEQ_1:46;
reconsider g = g as FinSequence of (Polynom-Ring L) by A6, FINSEQ_1:36;
A2c: dom f = Seg (n + 1) by A1, FINSEQ_1:def 3;
1 <= n + 1 by NAT_1:11;
then A2a: n + 1 in dom f by A2c;
A2c: n + 1 = (len g) + (len <*u*>) by A1, A6, FINSEQ_1:22
.= (len g) + 1 by FINSEQ_1:40 ;
A2b: f . (n + 1) = u by A2c, A6, FINSEQ_1:42;
then consider z being Element of L such that
U: u = rpoly (1,z) by A1, A2a;
reconsider u = u as Element of (Polynom-Ring L) by U, POLYNOM3:def 10;
reconsider q = Product g as Polynomial of L by POLYNOM3:def 10;
Product f = (Product g) * u by A6, GROUP_4:6
.= q *' (rpoly (1,z)) by U, POLYNOM3:def 10 ;
then A4: eval (p,x) = (eval (q,x)) * (eval ((rpoly (1,z)),x)) by A2, POLYNOM4:24;

A10: 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 C1: i in dom g ; :: thesis: ex z being Element of L st g . i = rpoly (1,z)
C2: dom g c= dom f by A6, FINSEQ_1:26;
g . i = f . i by C1, A6, FINSEQ_1:def 7;
hence ex z being Element of L st g . i = rpoly (1,z) by C1, C2, A1; :: 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 A4, A3, 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
B1: ( i in dom g & g . i = rpoly (1,x) ) by A2c, A10, IV;
B2: dom g c= dom f by A6, FINSEQ_1:26;
f . i = rpoly (1,x) by B1, A6, FINSEQ_1:def 7;
hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by B2, B1; :: 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 A2a, A2b, U; :: 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;

I: for n being Nat holds S₁[n] from NAT_1:sch 2(IA, IS);
len f is Nat ;
hence ex i being Nat st
( i in dom f & f . i = rpoly (1,x) ) by A0, AS1, AS2, I; :: 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 A; :: thesis: verum