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
( k < n & 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
( k < n & g = g1 |^ k & g = k mod n ) )
assume g1 = 1 ; :: thesis: ex k being Nat st
( k < n & g = g1 |^ k & g = k mod n )
then consider k1 being Nat such that
A1: ( g = g1 |^ k1 & g = k1 mod n ) by ThINTGroupOrd;
reconsider k = k1 mod n as Nat ;
take k ; :: thesis: ( k < n & g = g1 |^ k & g = k mod n )
thus k < n by NAT_D:1; :: thesis: ( g = g1 |^ k & g = k mod n )
consider t being Nat such that
A2: ( k1 = (n * t) + k & k < n ) by NAT_D:def 2;
thus g = g1 |^ k1 by A1
.= g1 |^ ((n * t) + k) by A2
.= (g1 |^ (n * t)) * (g1 |^ k) by GROUP_1:33
.= ((g1 |^ n) |^ t) * (g1 |^ k) by GROUP_1:35
.= ((g1 |^ (card (INT.Group n))) |^ t) * (g1 |^ k)
.= ((1_ (INT.Group n)) |^ t) * (g1 |^ k) by GR_CY_1:9
.= (1_ (INT.Group n)) * (g1 |^ k) by GROUP_1:31
.= g1 |^ k by GROUP_1:def 4 ; :: thesis: g = k mod n
k < n by NAT_D:1;
then k = k mod n by NAT_D:24;
hence g = k mod n by A1; :: thesis: verum