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

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