let n be Element of NAT ; :: thesis: ( n > 0 implies 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 )
assume A1: n > 0 ; :: 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 A2: INT.Group n = multMagma(# (Segm n),(addint n) #) by Def6;
0 + 1 < n + 1 by A1, XREAL_1:8;
then A3: n >= 1 by NAT_1:13;

now

per cases ( n = 1 or n > 1 ) by A3, 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 A2, Th36, CARD_1:87
.= the carrier of ((1). (INT.Group n)) by GROUP_2:def 7 ;
then INT.Group n = (1). (INT.Group n) by GROUP_2:70;
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 Th41; :: 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 g' = 1 as Element of Segm n by NAT_1:45;
reconsider g = g' as Element of (INT.Group n) by A2;
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 b' = b as Element of NAT by A2, Lm1;
defpred S₁[ Element of NAT ] means g |^ $1 = $1 mod n;
g |^ 0 = 1_ (INT.Group n) by GROUP_1:43
.= 0 by A1, Th36
.= 0 mod n by NAT_D:26 ;
then A4: S₁[ 0 ] ;
A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
k mod n < n by A1, NAT_D:1;
then reconsider e = k mod n as Element of Segm n by NAT_1:45;
assume A6: g |^ k = k mod n ; :: thesis: S₁[k + 1]
g |^ (k + 1) = (g |^ k) * (g |^ 1) by GROUP_1:63
.= (g |^ k) * g by GROUP_1:44
.= (e + g') mod n by A2, A6, Def5
.= (k + 1) mod n by NAT_D:22 ;
hence S₁[k + 1] ; :: thesis: verum

end;

A7: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A5);
A8: b' < n by A2, NAT_1:45;
A9: g |^ b' = b' mod n by A7
.= b by A8, NAT_D:24 ;
reconsider b' = b' as Integer ;
take b' ; :: thesis: b = g |^ b'
thus b = g |^ b' by A9; :: 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