let F be Field; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F)
for q being Element of the carrier of (Polynom-Ring F) holds
( not q divides p or q is unital or q is_associated_to p )
let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: for q being Element of the carrier of (Polynom-Ring F) holds
( not q divides p or q is unital or q is_associated_to p )
let q be Element of the carrier of (Polynom-Ring F); :: thesis: ( not q divides p or q is unital or q is_associated_to p )
assume AS: q divides p ; :: thesis: ( q is unital or q is_associated_to p )
then consider r being Polynomial of F such that
C: q *' r = p by RING_4:1;

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

suppose q is zero ; :: thesis: ( q is unital or q is_associated_to p )

hence ( q is unital or q is_associated_to p ) by C; :: thesis: verum

end;

suppose D: not q is zero ; :: thesis: ( q is unital or q is_associated_to p )

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

suppose deg q < 1 ; :: thesis: ( q is unital or q is_associated_to p )

then (deg q) + 1 <= 1 by INT_1:7;
then ((deg q) + 1) - 1 <= 1 - 1 by XREAL_1:9;
then q is constant by RING_4:def 4;
hence ( q is unital or q is_associated_to p ) by D; :: thesis: verum

end;

suppose A: deg q >= deg p ; :: thesis: ( q is unital or q is_associated_to p )

deg q <= deg p by AS, RING_5:13;
then B: deg q = deg p by A, XXREAL_0:1;
r <> 0_. F by C;
then deg p = (deg p) + (deg r) by D, C, B, HURWITZ:23;
then reconsider r = r as constant Element of the carrier of (Polynom-Ring F) by RING_4:def 4, POLYNOM3:def 10;
F: not r is zero by C;
q * r = p by C, POLYNOM3:def 10;
hence ( q is unital or q is_associated_to p ) by F, GCD_1:18; :: thesis: verum

end;

end;

end;

end;