let R be domRing; :: thesis: for p being monic Element of the carrier of (Polynom-Ring R) st deg p = 1 holds
p is irreducible
let p be monic 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 (len p) -' 1 = (1 + 1) -' 1
.= 1 by NAT_D:34 ;
then LC p = p . 1 ;
then E: p . 1 = 1. R by RATFUNC1:def 7;
p <> 0_. R ;
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 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 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;
q = u * (1_. R) by LX1, C1;
then q *' r = u * ((1_. R) *' r) by poly2
.= u * r by poly1 ;
then u * (r . 1) = (q *' r) . 1 by POLYNOM5:def 4
.= 1. R by H1, POLYNOM3:def 10, E ;
then u divides 1. R ;
then u is Unit of R by GCD_1:def 20;
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;
C3: r = u * (1_. R) by LX1, C1;
q *' r = u * ((1_. R) *' q) by C3, poly2
.= u * q by poly1 ;
then u * (q . 1) = (q *' r) . 1 by POLYNOM5:def 4
.= 1. R by H1, POLYNOM3:def 10, E ;
then u divides 1. R ;
then u is Unit of R by GCD_1:def 20;
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