theorem Th86: :: GROUP_24:81

for n being non zero Nat
for x being Element of (INT.Group n) holds x " = x |^ (n - 1)