let F be Field; :: thesis: for p being Element of the carrier of (Polynom-Ring F) st deg p = 3 holds
( p is reducible iff p is with_roots )
let p be Element of the carrier of (Polynom-Ring F); :: thesis: ( deg p = 3 implies ( p is reducible iff p is with_roots ) )
assume A: deg p = 3 ; :: 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;
( q <> 0_. F & r <> 0_. F ) by B2;
then B4: deg p = (deg q) + (deg r) by B2, HURWITZ:23;
B5: deg q < 2 + 1 by B1, A;
( deg q <= 2 implies not not deg q = 0 & ... & not deg q = 2 ) by B3;

per cases then ( deg q = 0 or deg q = 1 or deg q = 2 ) by B5, B3, NAT_1:13;

suppose deg q = 0 ; :: thesis: p is with_roots

hence p is with_roots by B1; :: thesis: verum

end;

suppose deg q = 1 ; :: thesis: p is with_roots

then q is linear by FIELD_5:def 1;
hence p is with_roots by B2; :: thesis: verum

end;

suppose deg q = 2 ; :: thesis: p is with_roots

then r is linear by B4, A, FIELD_5:def 1;
hence p is with_roots by B2; :: thesis: verum

end;

end;

end;

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