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