let F be finite Field; :: thesis: F is perfect
set p = Char F;
reconsider F = F as finite Char F -characteristic Field by RING_3:def 6;
H: the carrier of (F |^ (Char F)) = { (a |^ (Char F)) where a is Element of F : verum } by deffp;

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

let o be object ; :: thesis: ( o in the carrier of F implies o in the carrier of (F |^ (Char F)) )
assume o in the carrier of F ; :: thesis: o in the carrier of (F |^ (Char F))
then reconsider a = o as Element of F ;
consider b being Element of F such that
I: b |^ (Char F) = a by Fpp1;
thus o in the carrier of (F |^ (Char F)) by I, H; :: thesis: verum

end;

then A: the carrier of F c= the carrier of (F |^ (Char F)) ;
then J: [: the carrier of F, the carrier of F:] c= [: the carrier of (F |^ (Char F)), the carrier of (F |^ (Char F)):] by ZFMISC_1:96;
B: the addF of (F |^ (Char F)) || the carrier of F = ( the addF of F || the carrier of (F |^ (Char F))) || the carrier of F by deffp
.= the addF of F || the carrier of F by J, FUNCT_1:51 ;
C: the multF of (F |^ (Char F)) || the carrier of F = ( the multF of F || the carrier of (F |^ (Char F))) || the carrier of F by deffp
.= the multF of F || the carrier of F by J, FUNCT_1:51 ;
( 1. F = 1. (F |^ (Char F)) & 0. F = 0. (F |^ (Char F)) ) by deffp;
then F == F |^ (Char F) by A, B, C, EC_PF_1:def 1;
hence F is perfect by Fpp; :: thesis: verum