let F be Field; :: thesis: ( F is algebraic-closed iff for p being non constant monic Polynomial of F holds p is Ppoly of F )

now :: thesis: ( ( for p being non constant monic Polynomial of F holds p is Ppoly of F ) implies F is algebraic-closed )

hence
( F is algebraic-closed iff for p being non constant monic Polynomial of F holds p is Ppoly of F )
by cc3; :: thesis: verumassume AS:
for p being non constant monic Polynomial of F holds p is Ppoly of F
; :: thesis: F is algebraic-closed

end;now :: thesis: for p being Polynomial of F st len p > 1 holds

p is with_roots

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

let p be Polynomial of F; :: thesis: ( len p > 1 implies p is with_roots )

assume A: len p > 1 ; :: thesis: p is with_roots

then B: not p is zero by POLYNOM4:3;

set np = NormPolynomial p;

((len (NormPolynomial p)) - 1) + 1 > 1 by A, POLYNOM5:57;

then (len (NormPolynomial p)) - 1 >= 1 by NAT_1:13;

then ( not NormPolynomial p is constant & NormPolynomial p is monic ) by B, HURWITZ:def 2;

then reconsider np = NormPolynomial p as Ppoly of F by AS;

np is with_roots ;

hence p is with_roots by A, POLYNOM5:60; :: thesis: verum

end;assume A: len p > 1 ; :: thesis: p is with_roots

then B: not p is zero by POLYNOM4:3;

set np = NormPolynomial p;

((len (NormPolynomial p)) - 1) + 1 > 1 by A, POLYNOM5:57;

then (len (NormPolynomial p)) - 1 >= 1 by NAT_1:13;

then ( not NormPolynomial p is constant & NormPolynomial p is monic ) by B, HURWITZ:def 2;

then reconsider np = NormPolynomial p as Ppoly of F by AS;

np is with_roots ;

hence p is with_roots by A, POLYNOM5:60; :: thesis: verum