let F be Field; :: thesis: for p being Element of the carrier of (Polynom-Ring F) st deg p = 2 holds
( p is reducible iff p is with_roots )
let p be Element of the carrier of (Polynom-Ring F); :: thesis: ( deg p = 2 implies ( p is reducible iff p is with_roots ) )
assume A: deg p = 2 ; :: thesis: ( p is reducible iff p is with_roots )
then reconsider p = p as non constant non linear Element of the carrier of (Polynom-Ring F) by FIELD_5:def 1, RING_4:def 4;

now :: thesis: ( p is reducible implies p is with_roots )

assume B0: p is reducible ; :: thesis: p is with_roots
( p <> 0_. F & p is not Unit of (Polynom-Ring F) ) ;
then consider q being Element of the carrier of (Polynom-Ring F) such that
B1: ( q divides p & 1 <= deg q & deg q < deg p ) by B0, RING_4:41;
consider r being Polynomial of F such that
B2: p = q *' r by B1, RING_4:1;
B3: deg q is Element of NAT by B1, INT_1:3;
( 1 <= deg q & deg q < 1 + 1 ) by B1, A;
then ( 1 <= deg q & deg q <= 1 ) by B3, NAT_1:13;
then q is linear by XXREAL_0:1, FIELD_5:def 1;
hence p is with_roots by B2; :: thesis: verum

end;

hence ( p is reducible iff p is with_roots ) ; :: thesis: verum