let F be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) holds
( p is reducible iff ex q being monic Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p ) )
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( p is reducible iff ex q being monic Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p ) )

now :: thesis: ( p is reducible implies ex q being monic Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p ) )

assume p is reducible ; :: thesis: ex q being monic Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p )

per cases then ( p = 0_. F or p is Unit of (Polynom-Ring F) or ex q being Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p ) ) by RING_4:41;

suppose p = 0_. F ; :: thesis: ex q being monic Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p )

hence ex q being monic Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p ) ; :: thesis: verum

end;

suppose p is Unit of (Polynom-Ring F) ; :: thesis: ex q being monic Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p )

hence ex q being monic Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p ) ; :: thesis: verum

end;

suppose ex q being Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p ) ; :: thesis: ex q being monic Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p )

then consider q being Element of the carrier of (Polynom-Ring F) such that
A: ( q divides p & 1 <= deg q & deg q < deg p ) ;
set r = NormPolynomial q;
q <> 0_. F by A, HURWITZ:20;
then C: not q is zero by UPROOTS:def 5;
deg (NormPolynomial q) = deg q by REALALG3:11;
hence ex q being monic Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p ) by A, RING_4:25, C; :: thesis: verum

end;

end;

end;

hence ( p is reducible iff ex q being monic Element of the carrier of (Polynom-Ring F) st
( q divides p & 1 <= deg q & deg q < deg p ) ) by RING_4:41; :: thesis: verum