let F be Field; :: thesis: ( F is algebraic-closed iff for p being irreducible Element of the carrier of (Polynom-Ring F) holds deg p = 1 )

A: now :: thesis: ( F is algebraic-closed implies for p being irreducible Element of the carrier of (Polynom-Ring F) holds deg p = 1 )

assume B: F is algebraic-closed ; :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F) holds deg p = 1

now :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F) holds deg p = 1

let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: deg p = 1
set q = NormPolynomial p;
NormPolynomial p is irreducible by RING_4:28;
then deg (NormPolynomial p) = 1 by B, RING_4:46;
hence deg p = 1 by RING_4:27, RING_4:29; :: thesis: verum

end;

hence for p being irreducible Element of the carrier of (Polynom-Ring F) holds deg p = 1 ; :: thesis: verum

end;

now :: thesis: ( ( for p being irreducible Element of the carrier of (Polynom-Ring F) holds deg p = 1 ) implies F is algebraic-closed )

assume for p being irreducible Element of the carrier of (Polynom-Ring F) holds deg p = 1 ; :: thesis: F is algebraic-closed
then for p being monic Element of the carrier of (Polynom-Ring F) holds
( p is irreducible iff deg p = 1 ) by RING_4:42;
hence F is algebraic-closed by RING_4:46; :: thesis: verum

end;

hence ( F is algebraic-closed iff for p being irreducible Element of the carrier of (Polynom-Ring F) holds deg p = 1 ) by A; :: thesis: verum