let i, s, t, n be Nat; ( 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 )
; 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
( 0 < t & t <= k )
t is Element of NAT
by ORDINAL1:def 12;
hence
order ((i |^ s),n) = t
by A1, A4, A3, A6, A5, PEPIN:def 2; verum