let F be Field; :: thesis: ( F is algebraic-closed implies for p being non constant Polynomial of F holds p splits_in F )
assume B: F is algebraic-closed ; :: thesis: for p being non constant Polynomial of F holds p splits_in F

now :: thesis: for p being non constant Polynomial of F holds p splits_in F

let p be non constant Polynomial of F; :: thesis: p splits_in F
reconsider p1 = p as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
deg p1 > 0 by RATFUNC1:def 2;
then reconsider p1 = p as non constant Element of the carrier of (Polynom-Ring F) by RING_4:def 4;
set q = NormPolynomial p1;
deg (NormPolynomial p1) = deg p by RING_4:27, RING_4:29;
then reconsider q = NormPolynomial p1 as non constant monic Polynomial of F by RING_4:def 4, RATFUNC1:def 2;
reconsider q = q as Ppoly of F by B, RING_5:70;
C: LC p <> 0. F ;
q = ((LC p) ") * p by RING_4:23;
then (LC p) * q = ((LC p) * ((LC p) ")) * p by RING_4:11
.= (((LC p) ") * (LC p)) * p by GROUP_1:def 12
.= (1. F) * p by C, VECTSP_1:def 10
.= p ;
hence p splits_in F by FIELD_4:def 5; :: thesis: verum

end;

hence for p being non constant Polynomial of F holds p splits_in F ; :: thesis: verum