let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible )
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible )
defpred S₁[ Nat] means for p being non constant Element of the carrier of (Polynom-Ring F) st deg p = $1 holds
ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible );

IS: now :: thesis: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume AS1: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]

now :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) st deg p = k holds
ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible )

let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( deg p = k implies ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( b₂ divides q & b₂ is irreducible ) )
assume AS3: deg p = k ; :: thesis: ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( b₂ divides q & b₂ is irreducible )

per cases ( p is irreducible or not p is irreducible ) ;

suppose AS4: p is irreducible ; :: thesis: ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( b₂ divides q & b₂ is irreducible )

set q = NormPolynomial p;
p *' (1_. F) = p ;
then A: NormPolynomial p divides p by RING_4:25, RING_4:1;
NormPolynomial p is irreducible by AS4, RING_4:28;
hence ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible ) by A; :: thesis: verum

end;

suppose AS4: not p is irreducible ; :: thesis: ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( b₂ divides q & b₂ is irreducible )

p <> 0_. F ;
then consider q being Element of the carrier of (Polynom-Ring F) such that
A: ( q divides p & 1 <= deg q & deg q < deg p ) by AS4, RING_4:41;
reconsider m = deg q as Element of NAT by A, INT_1:3;
H: S₁[m] by AS1, A, AS3;
not q is constant by A, RING_4:def 4;
then consider r being monic non constant Element of the carrier of (Polynom-Ring F) such that
B: ( r divides q & r is irreducible ) by H;
consider s being Polynomial of F such that
C: q *' s = p by A, RING_4:1;
consider t being Polynomial of F such that
D: r *' t = q by B, RING_4:1;
r *' (s *' t) = p by C, D, POLYNOM3:33;
hence ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible ) by B, RING_4:1; :: thesis: verum

end;

end;

end;

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

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 4(IS);
reconsider n = deg p as Element of NAT ;
S₁[n] by I;
hence ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible ) ; :: thesis: verum