theorem :: FIELD_16:26

for p being Prime holds Frob (Z/ p) = id (Z/ p)