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
( 0 < k1 & k1 <= k ) ) & k2 > 0 & (i |^ k2) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
( 0 < k2 & 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
( 0 < k1 & k1 <= k ) ) & k2 > 0 & (i |^ k2) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
( 0 < k2 & k2 <= k ) ) ) ; :: thesis: k1 = k2
then ( k1 <= k2 & k2 <= k1 ) ;
hence k1 = k2 by XXREAL_0:1; :: thesis: verum