let F be Field; :: thesis: for p being Element of the carrier of (Polynom-Ring F) st deg p is odd holds
ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible & deg q is odd )
let p1 be Element of the carrier of (Polynom-Ring F); :: thesis: ( deg p1 is odd implies ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p1 & q is irreducible & deg q is odd ) )
assume AS: deg p1 is odd ; :: thesis: ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p1 & q is irreducible & deg q is odd )

per cases ( p1 is zero or not p1 is zero ) ;

suppose p1 is zero ; :: thesis: ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p1 & q is irreducible & deg q is odd )

then A: (X- (1. F)) *' (0_. F) = p1 by UPROOTS:def 5;
deg (X- (1. F)) = (2 * 0) + 1 by FIELD_5:def 1;
hence ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p1 & q is irreducible & deg q is odd ) by A, RING_4:1; :: thesis: verum

end;

suppose not p1 is zero ; :: thesis: ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p1 & q is irreducible & deg q is odd )

then reconsider p = p1 as non zero Element of the carrier of (Polynom-Ring F) ;
defpred S₁[ Nat] means for p being non zero Element of the carrier of (Polynom-Ring F) st deg p = (2 * $1) + 1 holds
ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible & deg q is odd );

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₁[b₁] )
assume AS1: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[b₁]

per cases ( k = 0 or k > 0 ) ;

suppose AS2: k = 0 ; :: thesis: S₁[b₁]

now :: thesis: for p being non zero Element of the carrier of (Polynom-Ring F) st deg p = (2 * 0) + 1 holds
ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible & deg q is odd )

let p be non zero Element of the carrier of (Polynom-Ring F); :: thesis: ( deg p = (2 * 0) + 1 implies ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible & deg q is odd ) )
set q = NormPolynomial p;
p *' (1_. F) = p ;
then A: NormPolynomial p divides p by RING_4:25, RING_4:1;
C: 1 = (2 * 0) + 1 ;
assume deg p = (2 * 0) + 1 ; :: thesis: ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible & deg q is odd )
then B: deg (NormPolynomial p) = 1 by lemdeg;
then NormPolynomial p is linear by FIELD_5:def 1;
hence ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible & deg q is odd ) by A, B, C; :: thesis: verum

end;

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

end;

suppose k > 0 ; :: thesis: S₁[b₁]

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

let p be non zero Element of the carrier of (Polynom-Ring F); :: thesis: ( deg p = (2 * k) + 1 implies ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( b₂ divides q & b₂ is irreducible & deg b₂ is odd ) )
assume AS3: deg p = (2 * k) + 1 ; :: thesis: ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( b₂ divides q & b₂ is irreducible & deg b₂ is odd )
then not p is constant by RING_4:def 4;
then consider q being monic non constant Element of the carrier of (Polynom-Ring F) such that
A: ( q divides p & q is irreducible ) by lem22;

per cases ( deg q is odd or deg q is even ) ;

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

hence ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible & deg q is odd ) by A; :: thesis: verum

end;

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

consider r being Polynomial of F such that
C: q *' r = p by A, RING_4:1;
( q <> 0_. F & r <> 0_. F ) by C;
then I: (deg q) + (deg r) = deg p by C, HURWITZ:23;
then deg r is odd by AS3, B;
then consider i being Integer such that
E: deg r = (2 * i) + 1 by ABIAN:1;

now :: thesis: not i < 0

assume E2: i < 0 ; :: thesis: contradiction
not r is zero by C;
hence contradiction by E, E2, INT_1:7; :: thesis: verum

end;

then reconsider i = i as Element of NAT by INT_1:3;
reconsider r = r as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
reconsider r = r as non zero Element of the carrier of (Polynom-Ring F) by C;
( deg r <= deg p & deg r <> deg p ) by C, I, RING_4:def 4, RING_4:1, RING_5:13;
then (2 * i) + 1 < (2 * k) + 1 by AS3, E, XXREAL_0:1;
then ((2 * i) + 1) - 1 < ((2 * k) + 1) - 1 by XREAL_1:9;
then (2 * i) - (2 * k) < (2 * k) - (2 * k) by XREAL_1:9;
then 2 * (i - k) < 0 ;
then i - k < 0 ;
then (i - k) + k < 0 + k by XREAL_1:6;
then consider s being monic non constant Element of the carrier of (Polynom-Ring F) such that
F: ( s divides r & s is irreducible & deg s is odd ) by E, AS1;
consider t being Polynomial of F such that
H: s *' t = r by F, RING_4:1;
s *' (t *' q) = p by H, C, POLYNOM3:33;
hence ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p & q is irreducible & deg q is odd ) by F, RING_4:1; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 4(IS);
consider i being Integer such that
H: deg p = (2 * i) + 1 by AS, ABIAN:1;
i >= 0 by H, INT_1:7;
then reconsider i = i as Element of NAT by INT_1:3;
deg p = (2 * i) + 1 by H;
hence ex q being monic non constant Element of the carrier of (Polynom-Ring F) st
( q divides p1 & q is irreducible & deg q is odd ) by I; :: thesis: verum

end;

end;