let k1, k2 be Element of NAT ; :: thesis: ( k1 > 0 & (i |^ k1) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
k1 <= k ) & k2 > 0 & (i |^ k2) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
k2 <= k ) implies k1 = k2 )
assume ( k1 > 0 & (i |^ k1) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
k1 <= k ) & k2 > 0 & (i |^ k2) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
k2 <= k ) ) ; :: thesis: k1 = k2
then ( k1 <= k2 & k2 <= k1 ) ;
hence k1 = k2 by XXREAL_0:1; :: thesis: verum