let p be Element of the carrier of (Polynom-Ring F); :: thesis: ( not p is linear & p is with_roots implies p is reducible )
assume AS: ( not p is linear & p is with_roots ) ; :: thesis: p is reducible
then consider a being Element of F such that
A: a is_a_root_of p by POLYNOM5:def 8;
consider q1 being Polynomial of F such that
B: p = (rpoly (1,a)) *' q1 by A, HURWITZ:33;
reconsider q = q1 as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
C: q divides p by B, RING_4:1;

per cases ( p = 0_. F or p <> 0_. F ) ;

suppose p = 0_. F ; :: thesis: p is reducible

hence p is reducible ; :: thesis: verum

end;

suppose L: p <> 0_. F ; :: thesis: p is reducible

then M: q1 <> 0_. F by B;
then D: deg p = (deg (rpoly (1,a))) + (deg q1) by B, HURWITZ:23
.= 1 + (deg q1) by HURWITZ:27 ;
reconsider degp = deg p, degq = deg q as Element of NAT by M, L, FIELD_1:1;
1 + degq >= 1 + 1 by D, AS, NAT_1:23;
then 1 <= degq by XREAL_1:6;
hence p is reducible by C, D, NAT_1:19, RING_4:40; :: thesis: verum

end;

end;