theorem LmINTGroupOrd3: :: GROUP_24:86

for n being non zero Nat
for g1 being Element of (INT.Group n) st g1 = 1 holds
for i being Nat holds g1 |^ i = i mod n