let n be non zero Nat; :: thesis: for g1 being Element of (INT.Group n) st g1 = 1 holds
for i, j being Nat holds
( g1 |^ i = g1 |^ j iff i mod n = j mod n )
let g1 be Element of (INT.Group n); :: thesis: ( g1 = 1 implies for i, j being Nat holds
( g1 |^ i = g1 |^ j iff i mod n = j mod n ) )
assume A1: g1 = 1 ; :: thesis: for i, j being Nat holds
( g1 |^ i = g1 |^ j iff i mod n = j mod n )
let i, j be Nat; :: thesis: ( g1 |^ i = g1 |^ j iff i mod n = j mod n )
thus ( g1 |^ i = g1 |^ j implies i mod n = j mod n ) :: thesis: ( i mod n = j mod n implies g1 |^ i = g1 |^ j )

proof

assume A2: g1 |^ i = g1 |^ j ; :: thesis: i mod n = j mod n
thus i mod n = g1 |^ i by A1, LmINTGroupOrd3
.= g1 |^ j by A2
.= j mod n by A1, LmINTGroupOrd3 ; :: thesis: verum

end;

assume A3: i mod n = j mod n ; :: thesis: g1 |^ i = g1 |^ j
thus g1 |^ i = g1 |^ ((n * (i div n)) + (i mod n)) by NAT_D:2
.= (g1 |^ (n * (i div n))) * (g1 |^ (i mod n)) by GROUP_1:33
.= ((g1 |^ (card (INT.Group n))) |^ (i div n)) * (g1 |^ (i mod n)) by GROUP_1:35
.= ((1_ (INT.Group n)) |^ (i div n)) * (g1 |^ (i mod n)) by GR_CY_1:9
.= (1_ (INT.Group n)) * (g1 |^ (i mod n)) by GROUP_1:31
.= ((1_ (INT.Group n)) |^ (j div n)) * (g1 |^ (i mod n)) by GROUP_1:31
.= ((1_ (INT.Group n)) |^ (j div n)) * (g1 |^ (j mod n)) by A3
.= ((g1 |^ (card (INT.Group n))) |^ (j div n)) * (g1 |^ (j mod n)) by GR_CY_1:9
.= (g1 |^ (n * (j div n))) * (g1 |^ (j mod n)) by GROUP_1:35
.= g1 |^ ((n * (j div n)) + (j mod n)) by GROUP_1:33
.= g1 |^ j by NAT_D:2 ; :: thesis: verum