let n be non zero Nat; :: thesis: for x being Element of (INT.Group n) holds x " = x |^ (n - 1)
let x be Element of (INT.Group n); :: thesis: x " = x |^ (n - 1)
set N = card (INT.Group n);

per cases ( n = 1 or n > 1 ) by NAT_1:53;

suppose n = 1 ; :: thesis: x " = x |^ (n - 1)

then A1: x = 1_ (INT.Group n) by Th77;
hence x " = 1_ (INT.Group n) by GROUP_1:8
.= (1_ (INT.Group n)) |^ (n - 1) by GROUP_1:31
.= x |^ (n - 1) by A1 ;
:: thesis: verum

end;

suppose n > 1 ; :: thesis: x " = x |^ (n - 1)

then A2: 1 mod (card (INT.Group n)) = 1 by PEPIN:5;
thus x " = (x |^ 1) " by GROUP_1:26
.= x |^ ((card (INT.Group n)) - (1 mod (card (INT.Group n)))) by GR_CY_1:10
.= x |^ (n - 1) by A2 ; :: thesis: verum

end;

end;