let R be Field; :: thesis: for p being Element of the carrier of (Polynom-Ring R) st deg p = 1 holds
p is irreducible
let p be Element of the carrier of (Polynom-Ring R); :: thesis: ( deg p = 1 implies p is irreducible )
set K = Polynom-Ring R;
reconsider x = p as Element of (Polynom-Ring R) ;
assume AS: deg p = 1 ; :: thesis: p is irreducible
then p <> 0_. R by HURWITZ:20;
then A: x <> 0. (Polynom-Ring R) by POLYNOM3:def 10;
B: x is not Unit of (Polynom-Ring R) by AS, T88;

now :: thesis: for a being Element of (Polynom-Ring R) holds
( not a divides x or a is Unit of (Polynom-Ring R) or a is_associated_to x )

let a be Element of (Polynom-Ring R); :: thesis: ( not a divides x or b₁ is Unit of (Polynom-Ring R) or b₁ is_associated_to x )
assume a divides x ; :: thesis: ( b₁ is Unit of (Polynom-Ring R) or b₁ is_associated_to x )
then consider b being Element of (Polynom-Ring R) such that
H1: a * b = x ;
reconsider q = a, r = b as Element of the carrier of (Polynom-Ring R) ;
q *' r = p by H1, POLYNOM3:def 10;
then H2: ( q <> 0_. R & r <> 0_. R ) by AS, HURWITZ:20, POLYNOM3:34;
then H4: (deg q) + (deg r) = deg (q *' r) by HURWITZ:23
.= 1 by AS, H1, POLYNOM3:def 10 ;

per cases ( deg q = 0 or deg q <> 0 ) ;

suppose C0: deg q = 0 ; :: thesis: ( b₁ is Unit of (Polynom-Ring R) or b₁ is_associated_to x )

then q is constant ;
then consider u being Element of R such that
C1: q = u | R by T11;
not u is zero by C1, C0, T11a;
hence ( a is Unit of (Polynom-Ring R) or a is_associated_to x ) by Th90, C1; :: thesis: verum

end;

suppose deg q <> 0 ; :: thesis: ( b₁ is Unit of (Polynom-Ring R) or b₁ is_associated_to x )

then deg q > 0 by H2, T8b;
then (deg q) + (deg r) > 0 + (deg r) by XREAL_1:6;
then r is constant by H4, NAT_1:14;
then consider u being Element of R such that
C1: r = u | R by T11;
not u is zero by C1, T6, H2;
then r is Unit of (Polynom-Ring R) by Th90, C1;
hence ( a is Unit of (Polynom-Ring R) or a is_associated_to x ) by H1, GCD_1:18; :: thesis: verum

end;

end;

end;

hence p is irreducible by A, B, RING_2:def 9; :: thesis: verum