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

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

assume B: for p being non constant Polynomial of 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 )
assume C: len p > 1 ; :: thesis: p is with_roots
deg p = (len p) - 1 by HURWITZ:def 2;
then ((deg p) + 1) - 1 > 1 - 1 by C, XREAL_1:9;
then not p is constant by RATFUNC1:def 2;
hence p is with_roots by B; :: 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 Polynomial of F holds p is with_roots ) ; :: thesis: verum