let i, s, t, n be Nat; :: thesis: ( n > 1 & i,n are_coprime & order (i,n) = s * t implies order ((i |^ s),n) = t )
assume A1: ( n > 1 & i,n are_coprime & order (i,n) = s * t ) ; :: thesis: order ((i |^ s),n) = t
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
t <= k

proof

let k be Nat; :: thesis: ( k > 0 & ((i |^ s) |^ k) mod n = 1 implies t <= k )
assume A7: ( k > 0 & ((i |^ s) |^ k) mod n = 1 ) ; :: thesis: t <= k
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 t <= k by A7, NAT_D:7; :: thesis: verum

end;

t is Element of NAT by ORDINAL1:def 12;
hence order ((i |^ s),n) = t by A1, A4, A3, A6, A5, PEPIN:def 2; :: thesis: verum