let K be finite strict Field; :: thesis: for SK1 being strict Subfield of K st card K = card SK1 holds
SK1 = K
let SK1 be strict Subfield of K; :: thesis: ( card K = card SK1 implies SK1 = K )
assume A1: card K = card SK1 ; :: thesis: SK1 = K
A2: the carrier of SK1 = the carrier of K
proof
assume A3: the carrier of SK1 <> the carrier of K ; :: thesis: contradiction
A4: the carrier of SK1 c= the carrier of K by Def1;
then the carrier of SK1 c< the carrier of K by A3, XBOOLE_0:def 8;
hence contradiction by A1, A4, CARD_2:48; :: thesis: verum
end;
K is Subfield of K by Th1;
hence SK1 = K by A2, Th8; :: thesis: verum