let p be Prime; :: thesis: for F being p -characteristic Field holds
( F is perfect iff Frob F is Automorphism of F )
let F be p -characteristic Field; :: thesis: ( F is perfect iff Frob F is Automorphism of F )
H: Char F = p by RING_3:def 6;

A: now :: thesis: ( F is perfect implies Frob F is Automorphism of F )

assume F is perfect ; :: thesis: Frob F is Automorphism of F
then B: F == F |^ p by FIELD_15:91;
C: rng (Frob F) c= the carrier of F by RELAT_1:def 19;

now :: thesis: for o being object st o in the carrier of F holds
o in rng (Frob F)

let o be object ; :: thesis: ( o in the carrier of F implies o in rng (Frob F) )
assume o in the carrier of F ; :: thesis: o in rng (Frob F)
then reconsider b = o as Element of F ;
( b in the carrier of (F |^ p) & the carrier of (F |^ p) = { (a |^ p) where a is Element of F : verum } ) by B, FIELD_15:def 1;
then consider a being Element of F such that
C: a |^ p = b ;
D: dom (Frob F) = the carrier of F by FUNCT_2:def 1;
(Frob F) . a = b by H, C, defFr;
hence o in rng (Frob F) by D, FUNCT_1:def 3; :: thesis: verum

end;

then Frob F is onto by C, TARSKI:2;
hence Frob F is Automorphism of F ; :: thesis: verum

end;

now :: thesis: ( Frob F is Automorphism of F implies F is perfect )

assume A: Frob F is Automorphism of F ; :: thesis: F is perfect
B: the carrier of (F |^ p) c= the carrier of F by EC_PF_1:def 1;

now :: thesis: for o being object st o in the carrier of F holds
o in the carrier of (F |^ p)

let o be object ; :: thesis: ( o in the carrier of F implies o in the carrier of (F |^ p) )
assume o in the carrier of F ; :: thesis: o in the carrier of (F |^ p)
then reconsider b = o as Element of F ;
rng (Frob F) = the carrier of F by A, FUNCT_2:def 3;
then consider a being object such that
C: ( a in dom (Frob F) & (Frob F) . a = b ) by FUNCT_1:def 3;
reconsider a = a as Element of F by C;
D: b = a |^ p by H, C, defFr;
the carrier of (F |^ p) = { (a |^ p) where a is Element of F : verum } by FIELD_15:def 1;
hence o in the carrier of (F |^ p) by D; :: thesis: verum

end;

then E: the carrier of F c= the carrier of (F |^ p) ;
then the carrier of F = the carrier of (F |^ p) by B, XBOOLE_0:def 10;
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 FIELD_15:def 1;
then F == F |^ p by E, EC_PF_1:def 1;
hence F is perfect by FIELD_15:91; :: thesis: verum

end;

hence ( F is perfect iff Frob F is Automorphism of F ) by A; :: thesis: verum