let F be Field; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F)
for q being monic Element of the carrier of (Polynom-Ring F) holds
( not q divides p or q = 1_. F or q = NormPolynomial p )
let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: for q being monic Element of the carrier of (Polynom-Ring F) holds
( not q divides p or q = 1_. F or q = NormPolynomial p )
let q be monic Element of the carrier of (Polynom-Ring F); :: thesis: ( not q divides p or q = 1_. F or q = NormPolynomial p )
assume AS: q divides p ; :: thesis: ( q = 1_. F or q = NormPolynomial p )

per cases then ( deg q < 1 or deg q >= deg p ) by RING_4:41;

suppose deg q < 1 ; :: thesis: ( q = 1_. F or q = NormPolynomial p )

then (deg q) + 1 <= 1 by INT_1:7;
then ((deg q) + 1) - 1 <= 1 - 1 by XREAL_1:9;
then consider a being Element of F such that
A: q = a | F by RING_4:def 4, RING_4:20;
1. F = LC q by RATFUNC1:def 7
.= a by A, RING_5:6 ;
hence ( q = 1_. F or q = NormPolynomial p ) by A, RING_4:14; :: thesis: verum

end;

suppose A: deg q >= deg p ; :: thesis: ( q = 1_. F or q = NormPolynomial p )

deg q <= deg p by AS, RING_5:13;
then B: deg q = deg p by A, XXREAL_0:1;
consider r being Polynomial of F such that
C: q *' r = p by AS, RING_4:1;
r <> 0_. F by C;
then deg p = (deg p) + (deg r) by C, B, HURWITZ:23;
then r is constant Element of the carrier of (Polynom-Ring F) by RING_4:def 4, POLYNOM3:def 10;
then consider a being Element of F such that
D: r = a | F by RING_4:20;
a = LC p

proof

reconsider lq = deg q as Element of NAT ;
consider s being FinSequence of the carrier of F such that
A2: len s = lq + 1 and
A3: (q *' r) . lq = Sum s and
A4: for k being Element of NAT st k in dom s holds
s . k = (q . (k -' 1)) * (r . ((lq + 1) -' k)) by POLYNOM3:def 9;
A5: lq = (len q) - 1 by HURWITZ:def 2;
then A6: (len q) - 1 = (len q) -' 1 by XREAL_0:def 2;
lq + 1 > 0 ;
then len q >= 0 + 1 by A5, INT_1:7;
then len q in Seg (len q) by FINSEQ_1:1;
then A7: len q in dom s by A2, A5, FINSEQ_1:def 3;
then A8: s /. (len q) = s . (len q) by PARTFUN1:def 6
.= (q . lq) * (r . ((lq + 1) -' (len q))) by A4, A5, A6, A7
.= (q . (deg q)) * (r . 0) by A5, NAT_2:8
.= (LC q) * (r . 0) by FIELD_6:2
.= (1. F) * (r . 0) by RATFUNC1:def 7
.= a by D, Th28 ;

now :: thesis: for i being Element of NAT st i in dom s & i <> len q holds
s /. i = 0. F

let i be Element of NAT ; :: thesis: ( i in dom s & i <> len q implies s /. i = 0. F )
assume A9: ( i in dom s & i <> len q ) ; :: thesis: s /. i = 0. F
then A10: s . i = (q . (i -' 1)) * (r . ((lq + 1) -' i)) by A4;
i in Seg (len q) by A2, A5, A9, FINSEQ_1:def 3;
then i <= len q by FINSEQ_1:1;
then (len q) - i in NAT by INT_1:5;
then (lq + 1) -' i = (len q) - i by A5, XREAL_0:def 2;
then (lq + 1) -' i <> 0 by A9;
then r . ((lq + 1) -' i) = 0. F by D, Th28;
hence s /. i = 0. F by A9, A10, PARTFUN1:def 6; :: thesis: verum

end;

hence a = Sum s by A8, A7, POLYNOM2:3
.= LC p by A3, C, B, FIELD_6:2 ;
:: thesis: verum

end;

then E: r = (LC p) * (1_. F) by D, RING_4:16;
((LC p) ") * p = q *' (((LC p) ") * r) by C, RING_4:10
.= q *' ((((LC p) ") * (LC p)) * (1_. F)) by E, RING_4:11
.= q *' ((1. F) * (1_. F)) by VECTSP_1:def 10
.= q ;
hence ( q = 1_. F or q = NormPolynomial p ) by RING_4:23; :: thesis: verum

end;

end;