now :: thesis: ( ( for p being monic non constant Element of the carrier of (Polynom-Ring F) holds p is with_roots ) implies F is algebraic-closed )

assume A: for p being monic non constant Element of the carrier of (Polynom-Ring F) holds p is with_roots ; :: thesis: F is algebraic-closed

now :: thesis: for p being Polynomial of F st len p > 1 holds
p is with_roots

let p be Polynomial of F; :: thesis: ( len p > 1 implies p is with_roots )
reconsider q = NormPolynomial p as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
assume B: len p > 1 ; :: thesis: p is with_roots
then (len p) - 1 > 1 - 1 by XREAL_1:9;
then deg p > 0 by HURWITZ:def 2;
then D: not p is constant by RATFUNC1:def 2;
len q > 1 by B, POLYNOM5:57;
then (len q) - 1 > 1 - 1 by XREAL_1:9;
then ( not q is constant & q is monic ) by D, HURWITZ:def 2;
then q is with_roots by A;
hence p is with_roots by B, POLYNOM5:60; :: thesis: verum

end;

hence F is algebraic-closed by POLYNOM5:def 9; :: thesis: verum

end;

hence ex b₁ being Element of the carrier of (Polynom-Ring F) st
( b₁ is monic & not b₁ is constant & not b₁ is with_roots ) ; :: thesis: verum