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

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