let F be Field; :: thesis: for p being non constant monic Polynomial of F
for q being non zero Polynomial of F st p *' q is Ppoly of F holds
p is Ppoly of F
let p be non constant monic Polynomial of F; :: thesis: for q being non zero Polynomial of F st p *' q is Ppoly of F holds
p is Ppoly of F
let q be non zero Polynomial of F; :: thesis: ( p *' q is Ppoly of F implies p is Ppoly of F )
assume AS: p *' q is Ppoly of F ; :: thesis: p is Ppoly of F
( p <> 0_. F & q <> 0_. F ) ;
then A1: deg (p *' q) = (deg p) + (deg q) by HURWITZ:23;
deg p > 0 by RATFUNC1:def 2;
then A: deg (p *' q) >= 1 + 0 by A1, NAT_1:14;
defpred S₁[ Nat] means for p being non constant monic Polynomial of F
for q being non zero Polynomial of F st deg (p *' q) = $1 & p *' q is Ppoly of F holds
p is Ppoly of F;

now :: thesis: for p being non constant monic Polynomial of F
for q being non zero Polynomial of F st deg (p *' q) = 1 & p *' q is Ppoly of F holds
p is Ppoly of F

let p be non constant monic Polynomial of F; :: thesis: for q being non zero Polynomial of F st deg (p *' q) = 1 & p *' q is Ppoly of F holds
p is Ppoly of F
let q be non zero Polynomial of F; :: thesis: ( deg (p *' q) = 1 & p *' q is Ppoly of F implies p is Ppoly of F )
assume B: ( deg (p *' q) = 1 & p *' q is Ppoly of F ) ; :: thesis: p is Ppoly of F
( p <> 0_. F & q <> 0_. F ) ;
then deg (p *' q) = (deg p) + (deg q) by HURWITZ:23;
then B1: deg p <= deg (p *' q) by NAT_1:12;
deg p > 0 by RATFUNC1:def 2;
then deg p >= deg (p *' q) by B, NAT_1:14;
then consider x, z being Element of F such that
A3: ( x <> 0. F & p = x * (rpoly (1,z)) ) by B, B1, XXREAL_0:1, HURWITZ:28;
x * (LC (rpoly (1,z))) = LC (x * (rpoly (1,z))) by RING_5:5
.= 1. F by A3, RATFUNC1:def 7 ;
then x * (1. F) = 1. F by RATFUNC1:def 7;
hence p is Ppoly of F by A3, RING_5:51; :: thesis: verum

end;

then IA: S₁[1] ;

IS: now :: thesis: for k being Nat st 1 <= k & S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( 1 <= k & S₁[k] implies S₁[k + 1] )
assume BB: 1 <= k ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for p being non constant monic Polynomial of F
for q being non zero Polynomial of F st deg (p *' q) = k + 1 & p *' q is Ppoly of F holds
p is Ppoly of F

let p be non constant monic Polynomial of F; :: thesis: for q being non zero Polynomial of F st deg (p *' q) = k + 1 & p *' q is Ppoly of F holds
b₂ is Ppoly of F
let q be non zero Polynomial of F; :: thesis: ( deg (p *' q) = k + 1 & p *' q is Ppoly of F implies b₁ is Ppoly of F )
assume B: ( deg (p *' q) = k + 1 & p *' q is Ppoly of F ) ; :: thesis: b₁ is Ppoly of F
then ( LC p = 1. F & LC (p *' q) = 1. F ) by RATFUNC1:def 7;
then B0: 1. F = (1. F) * (LC q) by NIVEN:46;
then B0a: q is monic by RATFUNC1:def 7;
consider a being Element of F such that
B1: a is_a_root_of p *' q by B, POLYNOM5:def 8;
0. F = eval ((p *' q),a) by B1, POLYNOM5:def 7
.= (eval (p,a)) * (eval (q,a)) by POLYNOM4:24 ;

per cases then ( eval (q,a) = 0. F or eval (p,a) = 0. F ) by VECTSP_2:def 1;

suppose eval (q,a) = 0. F ; :: thesis: b₁ is Ppoly of F

then consider s being Polynomial of F such that
B2: q = (rpoly (1,a)) *' s by HURWITZ:33, POLYNOM5:def 7;
B3: not s is zero by B2;
B6: ( s <> 0_. F & p <> 0_. F ) by B2;
then deg q = (deg (rpoly (1,a))) + (deg s) by B2, HURWITZ:23
.= 1 + (deg s) by HURWITZ:27 ;
then B4: deg (p *' s) = (deg p) + ((deg q) - 1) by B6, HURWITZ:23
.= ((deg p) + (deg q)) - 1
.= (deg (p *' q)) - 1 by B6, HURWITZ:23
.= k by B ;
1. F = (LC (rpoly (1,a))) * (LC s) by B0, B2, NIVEN:46
.= (1. F) * (LC s) by RING_5:9 ;
then s is monic by RATFUNC1:def 7;
then B5: ( not p *' s is constant & p *' s is monic ) by BB, B4, RATFUNC1:def 2;
p *' q = (rpoly (1,a)) *' (p *' s) by B2, POLYNOM3:33;
then p *' s is Ppoly of F by B, B5, lemppolspl3b;
hence p is Ppoly of F by B3, B4, IV; :: thesis: verum

end;

suppose eval (p,a) = 0. F ; :: thesis: b₁ is Ppoly of F

then consider s being Polynomial of F such that
B2: p = (rpoly (1,a)) *' s by POLYNOM5:def 7, HURWITZ:33;
reconsider s = s as non zero Polynomial of F by B2;
B6: s <> 0_. F ;
then deg p = (deg (rpoly (1,a))) + (deg s) by B2, HURWITZ:23
.= 1 + (deg s) by HURWITZ:27 ;
then B4: deg (q *' s) = (deg q) + ((deg p) - 1) by B6, HURWITZ:23
.= ((deg p) + (deg q)) - 1
.= (deg (p *' q)) - 1 by B6, HURWITZ:23
.= k by B ;
B5: p *' q = (rpoly (1,a)) *' (s *' q) by B2, POLYNOM3:33;
B7b: 1. F = LC p by RATFUNC1:def 7
.= (LC (rpoly (1,a))) * (LC s) by B2, NIVEN:46
.= (1. F) * (LC s) by RING_5:9 ;
then B7a: s is monic by RATFUNC1:def 7;
reconsider s1 = s as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;

per cases ( deg s >= 1 or deg s < 1 ) ;

suppose K: deg s >= 1 ; :: thesis: b₁ is Ppoly of F

then B8a: not s is constant by RATFUNC1:def 2;
deg (s *' q) = (deg s) + (deg q) by B6, HURWITZ:23;
then not s *' q is constant by K, RATFUNC1:def 2;
then s *' q is Ppoly of F by B, B5, B7a, B0a, lemppolspl3b;
then B9: s is Ppoly of F by B4, B7a, B8a, IV;
rpoly (1,a) is Ppoly of F by RING_5:51;
hence p is Ppoly of F by B9, B2, RING_5:52; :: thesis: verum

end;

suppose deg s < 1 ; :: thesis: b₁ is Ppoly of F

then deg s = 0 by NAT_1:14;
then consider b being Element of F such that
B8: s1 = b | F by RING_4:def 4, RING_4:20;
B9: s = b * (1_. F) by B8, RING_4:16;
then LC s = b * (LC (1_. F)) by RING_5:5
.= b * (1. F) by RATFUNC1:def 7 ;
hence p is Ppoly of F by B7b, B9, B2, RING_5:51; :: thesis: verum

end;

end;

end;

end;

end;

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

end;

for i being Nat st 1 <= i holds
S₁[i] from NAT_1:sch 8(IA, IS);
hence p is Ppoly of F by A, AS; :: thesis: verum