let n be non zero Nat; :: thesis: ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1
0 + 1 < n + 1 by XREAL_1:6;
then A1: n >= 1 by NAT_1:13;

now :: thesis: ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1

per cases ( n = 1 or n > 1 ) by A1, XXREAL_0:1;

suppose n = 1 ; :: thesis: ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1

then the carrier of (INT.Group n) = {(1_ (INT.Group n))} by Th14, CARD_1:49
.= the carrier of ((1). (INT.Group n)) by GROUP_2:def 7 ;
then INT.Group n = (1). (INT.Group n) by GROUP_2:61;
hence ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1 by Th17; :: thesis: verum

end;

suppose n > 1 ; :: thesis: ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1

then reconsider g9 = 1 as Element of Segm n by NAT_1:44;
reconsider g = g9 as Element of (INT.Group n) ;
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1

proof

let b be Element of (INT.Group n); :: thesis: ex j1 being Integer st b = g |^ j1
reconsider b9 = b as Element of NAT by Lm1;
defpred S₁[ Nat] means g |^ $1 = $1 mod n;
A2: b9 < n by NAT_1:44;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: g |^ k = k mod n ; :: thesis: S₁[k + 1]
k mod n < n by NAT_D:1;
then reconsider e = k mod n as Element of Segm n by NAT_1:44;
g |^ (k + 1) = (g |^ k) * (g |^ 1) by GROUP_1:33
.= (g |^ k) * g by GROUP_1:26
.= (e + g9) mod n by A4, Def4
.= (k + 1) mod n by NAT_D:22 ;
hence S₁[k + 1] ; :: thesis: verum

end;

g |^ 0 = 1_ (INT.Group n) by GROUP_1:25
.= 0 by Th14
.= 0 mod n by NAT_D:26 ;
then A5: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A3);
then A6: g |^ b9 = b9 mod n
.= b by A2, NAT_D:24 ;
reconsider b9 = b9 as Integer ;
take b9 ; :: thesis: b = g |^ b9
thus b = g |^ b9 by A6; :: thesis: verum

end;

hence ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1 ; :: thesis: verum

end;

end;

end;

hence ex g being Element of (INT.Group n) st
for b being Element of (INT.Group n) ex j1 being Integer st b = g |^ j1 ; :: thesis: verum