let p be Prime; :: thesis: for F being p -characteristic Field holds
( F is perfect iff F == F |^ p )
let F be p -characteristic Field; :: thesis: ( F is perfect iff F == F |^ p )

A: now :: thesis: ( not F == F |^ p implies not F is perfect )

assume A1: not F == F |^ p ; :: thesis: not F is perfect
set a = the Element of the carrier of F \ the carrier of (F |^ p);
A2: the carrier of (F |^ p) c= the carrier of F by EC_PF_1:def 1;

now :: thesis: not the carrier of (F |^ p) = the carrier of F

assume B: the carrier of (F |^ p) = the carrier of F ; :: thesis: contradiction
then ( the addF of (F |^ p) = the addF of F || the carrier of F & the multF of (F |^ p) = the multF of F || the carrier of F & 1. (F |^ p) = 1. F & 0. (F |^ p) = 0. F ) by deffp;
hence contradiction by B, A1; :: thesis: verum

end;

then the carrier of (F |^ p) c< the carrier of F by A2, XBOOLE_0:def 8;
then A3: the carrier of F \ the carrier of (F |^ p) <> {} by XBOOLE_1:105;
then reconsider a = the Element of the carrier of F \ the carrier of (F |^ p) as Element of F by XBOOLE_0:def 5;
not a in F |^ p by A3, XBOOLE_0:def 5;
then ( X^ (p,a) is irreducible & X^ (p,a) is inseparable ) by contr;
hence not F is perfect ; :: thesis: verum

end;

now :: thesis: ( F == F |^ p implies F is perfect )

assume A0: F == F |^ p ; :: thesis: F is perfect

now :: thesis: F is perfect

assume not F is perfect ; :: thesis: contradiction
then consider q being irreducible Element of the carrier of (Polynom-Ring F) such that
A1: q is inseparable ;
consider E being FieldExtension of F such that
A2: ( q splits_in E & ex a being Element of E st
( a is_a_root_of q,E & multiplicity (q,a) <> 1 ) ) by A1, ThSep0;
consider a being Element of E such that
A3: ( a is_a_root_of q,E & multiplicity (q,a) <> 1 ) by A2;
multiplicity (q,a) >= 1 by A3, mulzero;
then multiplicity (q,a) > 1 by A3, XXREAL_0:1;
then A4: (Deriv F) . q = 0_. F by A2, lemsep1;

now :: thesis: for i being Nat st i in Support q holds
( p divides i & ex a being Element of F st a |^ p = q . i )

let i be Nat; :: thesis: ( i in Support q implies ( p divides i & ex a being Element of F st a |^ p = q . i ) )
assume i in Support q ; :: thesis: ( p divides i & ex a being Element of F st a |^ p = q . i )
hence p divides i by A4, DP0; :: thesis: ex a being Element of F st a |^ p = q . i
q . i in the carrier of (F |^ p) by A0;
then q . i in { (a |^ p) where a is Element of F : verum } by deffp;
hence ex a being Element of F st a |^ p = q . i ; :: thesis: verum

end;

then consider r being Element of the carrier of (Polynom-Ring F) such that
A5: r |^ p = q by DP1;
reconsider r = r as non constant Element of the carrier of (Polynom-Ring F) by A5;
H: r |^ ((p - 1) + 1) = (r |^ (p - 1)) * (r |^ 1) by BINOM:10
.= (r |^ (p - 1)) * r by BINOM:8
.= (r `^ (p - 1)) *' r by POLYNOM3:def 10 ;
A6: 0 + 1 <= deg r by INT_1:7, RING_4:def 4;
( r <> 0_. F & r `^ (p - 1) <> 0_. F ) ;
then K: deg q = (deg (r `^ (p - 1))) + (deg r) by A5, H, HURWITZ:23
.= ((p - 1) * (deg r)) + (deg r) by t1
.= p * (deg r) ;

now :: thesis: not deg r >= deg q

assume deg r >= deg q ; :: thesis: contradiction
then deg q >= p * (deg q) by K, XREAL_1:64;
then (deg q) / (deg q) >= (p * (deg q)) / (deg q) by XREAL_1:64;
then L: 1 >= (p * (deg q)) / (deg q) by K, A6, XCMPLX_1:60;
(p * (deg q)) / (deg q) = p * ((deg q) / (deg q))
.= p * 1 by K, A6, XCMPLX_1:60 ;
hence contradiction by L, INT_2:def 4; :: thesis: verum

end;

hence contradiction by H, A5, A6, RING_4:1, RING_4:40; :: thesis: verum

end;

hence F is perfect ; :: thesis: verum

end;

hence ( F is perfect iff F == F |^ p ) by A; :: thesis: verum