theorem Frobcard: :: FIELD_16:64

for p being Prime
for n being non zero Nat
for F being Field st card F = p |^ n holds
card { ((Frob F) `^ m) where m is Nat : ( 0 <= m & m <= n - 1 ) } = n