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 )
assume AS: for p being non constant monic Polynomial of F holds p is Ppoly of F ; :: 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 )
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;
hence F is algebraic-closed by POLYNOM5:def 9; :: thesis: verum
end;
hence ( F is algebraic-closed iff for p being non constant monic Polynomial of F holds p is Ppoly of F ) by cc3; :: thesis: verum