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 S1[ Nat] means g |^ $1 = $1 mod n;
A2: b9 < n by NAT_1:44;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: g |^ k = k mod n ; :: thesis: S1[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 S1[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: S1[ 0 ] ;
for k being Nat holds S1[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