let F be algebraic-closed Field; :: thesis: F is perfect

now :: thesis: for p being irreducible Element of the carrier of (Polynom-Ring F) holds p is separable

let p be irreducible Element of the carrier of (Polynom-Ring F); :: thesis: p is separable
B: deg p = 1 by FIELD_12:21;

now :: thesis: for a being Element of the SplittingField of p holds not multiplicity (p,a) > 1

let a be Element of the SplittingField of p; :: thesis: not multiplicity (p,a) > 1
assume A: multiplicity (p,a) > 1 ; :: thesis: contradiction
set K = the SplittingField of p;
reconsider q = p as Polynomial of the SplittingField of p by FIELD_4:8;
p <> 0_. F ;
then q <> 0_. the SplittingField of p by FIELD_4:12;
then reconsider q = q as non zero Polynomial of the SplittingField of p by UPROOTS:def 5;
D: deg q >= multiplicity (q,a) by ro00;
reconsider q1 = q as Element of the carrier of (Polynom-Ring the SplittingField of p) by POLYNOM3:def 10;
deg q1 = deg p by FIELD_4:20;
hence contradiction by D, B, A, FIELD_14:def 6; :: thesis: verum

end;

hence p is separable by ThSep01; :: thesis: verum

end;

hence F is perfect ; :: thesis: verum