let n be non zero Nat; :: thesis: for g, g1 being Element of (INT.Group n) st g1 = 1 holds
ex k being Nat st
( g = g1 |^ k & g = k mod n )
let g, g1 be Element of (INT.Group n); :: thesis: ( g1 = 1 implies ex k being Nat st
( g = g1 |^ k & g = k mod n ) )
assume A1: g1 = 1 ; :: thesis: ex k being Nat st
( g = g1 |^ k & g = k mod n )

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

suppose n = 1 ; :: thesis: ex k being Nat st
( g = g1 |^ k & g = k mod n )

then INT.Group n is trivial ;
then B1: g = 1_ (INT.Group n) ;
take k = 0 ; :: thesis: ( g = g1 |^ k & g = k mod n )
thus g = g1 |^ k by B1, GROUP_1:25; :: thesis: g = k mod n
thus g = 0 by B1, GR_CY_1:14
.= k mod n by NAT_D:26 ; :: thesis: verum

end;

suppose A3: n > 1 ; :: thesis: ex k being Nat st
( g = g1 |^ k & g = k mod n )

g in the carrier of (INT.Group n) ;
then A4: g in Segm n by Th76;
reconsider k = g as Nat ;
A5: k < n by A4, NAT_1:44;
defpred S₁[ Nat] means ( $1 < n implies g1 |^ $1 = $1 mod n );
A6: S₁[ 0 ]

proof

( 0 < n implies g1 |^ 0 = 0 mod n )

proof

assume 0 < n ; :: thesis: g1 |^ 0 = 0 mod n
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;

hence S₁[ 0 ] ; :: thesis: verum

end;

A7: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume B1: S₁[j] ; :: thesis: S₁[j + 1]
assume B2: j + 1 < n ; :: thesis: g1 |^ (j + 1) = (j + 1) mod n
j < j + 1 by NAT_1:16;
then B3: j < n by B2, XXREAL_0:2;
then B4: j mod n = j by NAT_D:24;
1 in Segm n by A3, NAT_1:44;
then B5: ( 1 in Segm n & j in Segm n ) by B3, NAT_1:44;
g1 |^ (j + 1) = (g1 |^ j) * g1 by GROUP_1:34
.= (addint n) . ((j mod n),1) by A1, B1, B3, Th75
.= (addint n) . (j,1) by B4
.= (j + 1) mod n by B5, GR_CY_1:def 4 ;
hence g1 |^ (j + 1) = (j + 1) mod n ; :: thesis: verum

end;

A8: for j being Nat holds S₁[j] from NAT_1:sch 2(A6, A7);
take k ; :: thesis: ( g = g1 |^ k & g = k mod n )
A9: S₁[k] by A8;
hence g1 |^ k = k mod n by A5
.= g by A5, NAT_D:24 ;
:: thesis: g = k mod n
hence g = k mod n by A5, A9; :: thesis: verum

end;

end;