let s, t, n be Nat; :: thesis: ( n > 1 & s,n are_coprime & (s * t) mod n = 1 implies order (s,n) = order (t,n) )
assume A1: ( n > 1 & s,n are_coprime & (s * t) mod n = 1 ) ; :: thesis: order (s,n) = order (t,n)
set f = t gcd n;

A2: now :: thesis: t,n are_coprime

assume not t,n are_coprime ; :: thesis: contradiction
then A3: t gcd n <> 1 by INT_2:def 3;
t gcd n <> 0 by A1, INT_2:5;
then A4: t gcd n > 1 by A3, NAT_1:25;
A5: n divides (s * t) - 1 by A1, PEPIN:8;
A6: ( t gcd n divides t & t gcd n divides n ) by NAT_D:def 5;
then A7: t gcd n divides (s * t) - 1 by A5, INT_2:9;
t gcd n divides s * t by A6, NAT_D:9;
hence contradiction by A4, A7, INT_5:2, NAT_D:7; :: thesis: verum

end;

A8: order (s,n) > 0 by A1, PEPIN:def 2;
set M = s * t;
A9: (s * t) mod n = 1 mod n by A1, PEPIN:5;
then ((s * t) |^ (order (s,n))) mod n = (1 |^ (order (s,n))) mod n by INT_4:8
.= 1 mod n
.= 1 by A1, PEPIN:5 ;
then A10: ((s |^ (order (s,n))) * (t |^ (order (s,n)))) mod n = 1 by NEWTON:7;
(s |^ (order (s,n))) mod n = 1 by A1, PEPIN:def 2;
then A11: (t |^ (order (s,n))) mod n = 1 by A10, Th6;
for k being Nat st k > 0 & (t |^ k) mod n = 1 holds
order (s,n) <= k

proof

let k be Nat; :: thesis: ( k > 0 & (t |^ k) mod n = 1 implies order (s,n) <= k )
assume A12: ( k > 0 & (t |^ k) mod n = 1 ) ; :: thesis: order (s,n) <= k
((s * t) |^ k) mod n = (1 |^ k) mod n by A9, INT_4:8
.= 1 mod n
.= 1 by A1, PEPIN:5 ;
then ((s |^ k) * (t |^ k)) mod n = 1 by NEWTON:7;
then (s |^ k) mod n = 1 by A12, Th6;
hence order (s,n) <= k by A1, A12, PEPIN:def 2; :: thesis: verum

end;

hence order (s,n) = order (t,n) by A11, A8, A2, A1, PEPIN:def 2; :: thesis: verum