set Fp = F |^ p;
A: the carrier of (F |^ p) = { (a |^ p) where a is Element of F : verum } by deffp;

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

let o be object ; :: thesis: ( o in the carrier of (F |^ p) implies o in the carrier of F )
assume o in the carrier of (F |^ p) ; :: thesis: o in the carrier of F
then consider b being Element of F such that
H: o = b |^ p by A;
thus o in the carrier of F by H; :: thesis: verum

end;

then B: the carrier of (F |^ p) c= the carrier of F ;
( the addF of (F |^ p) = the addF of F || the carrier of (F |^ p) & the multF of (F |^ p) = the multF of F || the carrier of (F |^ p) & 1. (F |^ p) = 1. F & 0. (F |^ p) = 0. F ) by deffp;
hence F |^ p is strict Subfield of F by B, EC_PF_1:def 1; :: thesis: verum