let n be non zero Nat; :: thesis: for g1 being Element of (INT.Group n) st g1 = 1 holds
for i being Nat holds g1 |^ i = i mod n
let g1 be Element of (INT.Group n); :: thesis: ( g1 = 1 implies for i being Nat holds g1 |^ i = i mod n )
assume A1: g1 = 1 ; :: thesis: for i being Nat holds g1 |^ i = i mod n
defpred S₁[ Nat] means g1 |^ $1 = $1 mod n;
A2: S₁[ 0 ]

proof

thus g1 |^ 0 = 1_ (INT.Group n) by GROUP_1:25
.= 0 by GR_CY_1:14
.= 0 mod n by NAT_D:26 ; :: thesis: verum

end;

A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
( i mod n < n & i mod n in NAT ) by NAT_D:1;
then A5: i mod n in Segm n by NAT_1:44;

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

suppose A6: n = 1 ; :: thesis: S₁[i + 1]

then INT.Group n is trivial ;
then A7: g1 |^ (i + 1) = 1_ (INT.Group n)
.= 0 by GR_CY_1:14 ;
(i + 1) mod n = (i + 1) mod 1 by A6
.= (1 * (i + 1)) mod 1
.= 0 by NAT_D:13 ;
hence S₁[i + 1] by A7; :: thesis: verum

end;

suppose n > 1 ; :: thesis: S₁[i + 1]

then A7: 1 in Segm n by NAT_1:44;
g1 |^ (i + 1) = (g1 |^ i) * g1 by GROUP_1:34
.= (addint n) . ((i mod n),1) by A1, A4, Th75
.= ((i mod n) + 1) mod n by A5, A7, GR_CY_1:def 4
.= (i + 1) mod n by NAT_D:22 ;
hence S₁[i + 1] ; :: thesis: verum

end;

end;

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
hence for i being Nat holds g1 |^ i = i mod n ; :: thesis: verum