let p be Polynomial of F; :: thesis: ( p is linear implies p is with_roots )
assume p is linear ; :: thesis: p is with_roots
then consider x, z being Element of F such that
A: ( x <> 0. F & p = x * (rpoly (1,z)) ) by HURWITZ:28;
thus p is with_roots by A; :: thesis: verum