let F be Field; :: thesis: for p being Polynomial of F st deg p = 1 holds
p splits_in F
let p be Polynomial of F; :: thesis: ( deg p = 1 implies p splits_in F )
assume deg p = 1 ; :: thesis: p splits_in F
then consider x, z being Element of F such that
A1: ( x <> 0. F & p = x * (rpoly (1,z)) ) by HURWITZ:28;
reconsider x = x as non zero Element of F by A1, STRUCT_0:def 12;
reconsider q = rpoly (1,z) as Ppoly of F by RING_5:51;
p = x * q by A1;
hence p splits_in F ; :: thesis: verum