let p be Prime; :: thesis: for F being GaloisField of p holds F == Z/ p
let F be GaloisField of p; :: thesis: F == Z/ p
A: ( order F = p |^ 1 & Z/ p is Subfield of F ) by defGal;
then H: card F = card (Z/ p) by fresh3a;
reconsider X = the carrier of F, Y = the carrier of (Z/ p) as finite set ;
B: Y c= X by A, EC_PF_1:def 1;
then card (X \ Y) = (card X) - (card Y) by CARD_2:44
.= 0 by H ;
then X \ Y = {} ;
then the carrier of F c= the carrier of (Z/ p) by XBOOLE_0:def 5;
then E: the carrier of F = the carrier of (Z/ p) by B, XBOOLE_0:def 10;
( the addF of (Z/ p) = the addF of F || the carrier of (Z/ p) & the multF of (Z/ p) = the multF of F || the carrier of (Z/ p) & 1. F = 1. (Z/ p) & 0. F = 0. (Z/ p) ) by A, EC_PF_1:def 1;
hence F == Z/ p by E; :: thesis: verum