let i, s, t, n be Nat; :: thesis:
assume A1: ( n > 1 & i,n are_coprime & order (i,n) = s * t ) ; :: thesis:
then A2: i <> 0 by Th5;
A3: ( t <> 0 & s <> 0 ) by A1, PEPIN:def 2;
i gcd n = 1 by A1, INT_2:def 3;
then (i |^ s) gcd n = 1 by A2, A1, NAT_4:10;
then A4: i |^ s,n are_coprime by INT_2:def 3;
A5: ((i |^ s) |^ t) mod n = (i |^ (order (i,n))) mod n by A1, NEWTON:9
.= 1 by A1, PEPIN:def 2 ;
A6: for k being Nat st k > 0 & ((i |^ s) |^ k) mod n = 1 holds
( 0 < t & t <= k )

let k be Nat; :: thesis:
assume A7: ( k > 0 & ((i |^ s) |^ k) mod n = 1 ) ; :: thesis:
then A8: (i |^ (s * k)) mod n = 1 by NEWTON:9;
reconsider t = t, s = s, k = k as Element of NAT by ORDINAL1:def 12;
t * s divides k * s by A8, A1, PEPIN:47;
then t divides k by A3, PYTHTRIP:7;
hence ( 0 < t & t <= k ) by A3, A7, NAT_D:7; :: thesis:

end;