theorem lemAuthelp: :: FIELD_16:62

for p being Prime
for n being non zero Nat
for F being Field st card F = p |^ n holds
for k being Nat st 0 < k & k <= n - 1 holds
(Frob F) `^ k <> id F