set A = { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } ;
A3: { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } c= NAT

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } or a in NAT )
assume a in { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } ; :: thesis: a in NAT
then ex k being Element of NAT st
( k = a & k > 0 & (i |^ k) mod p = 1 ) ;
hence a in NAT ; :: thesis: verum

end;

i <> 0

proof

assume i = 0 ; :: thesis: contradiction
then i gcd p = p by NEWTON:52;
hence contradiction by A1, A2, INT_2:def 3; :: thesis: verum

end;

then A4: (i |^ (Euler p)) mod p = 1 by A1, A2, EULER_2:18;
Euler p <> 0 by A1, Th42;
then Euler p in { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } by A4;
then reconsider A = { k where k is Element of NAT : ( k > 0 & (i |^ k) mod p = 1 ) } as non empty Subset of NAT by A3;
set a = the Element of A;
defpred S₁[ set ] means $1 in A;
the Element of A is Element of NAT ;
then A5: ex kk being Nat st S₁[kk] ;
consider kk being Nat such that
A6: S₁[kk] and
A7: for n being Nat st S₁[n] holds
kk <= n from NAT_1:sch 5(A5);
take kk ; :: thesis: ( kk is Element of NAT & kk > 0 & (i |^ kk) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
kk <= k ) )
A8: for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
kk <= k

proof

let k be Nat; :: thesis: ( k > 0 & (i |^ k) mod p = 1 implies kk <= k )
assume A9: ( k > 0 & (i |^ k) mod p = 1 ) ; :: thesis: kk <= k
k in NAT by ORDINAL1:def 12;
then k in A by A9;
hence kk <= k by A7; :: thesis: verum

end;

ex k being Element of NAT st
( k = kk & k > 0 & (i |^ k) mod p = 1 ) by A6;
hence ( kk is Element of NAT & kk > 0 & (i |^ kk) mod p = 1 & ( for k being Nat st k > 0 & (i |^ k) mod p = 1 holds
kk <= k ) ) by A8; :: thesis: verum