let i, n be Nat; :: thesis: for fn being FinSequence of NAT st n > 1 & i,n are_coprime & len fn = order (i,n) & ( for d being Element of NAT st d in dom fn holds
fn . d = i |^ (d -' 1) ) holds
for d, e being Element of NAT st d in dom fn & e in dom fn & d <> e holds
not fn . d,fn . e are_congruent_mod n
let fn be FinSequence of NAT ; :: thesis: ( n > 1 & i,n are_coprime & len fn = order (i,n) & ( for d being Element of NAT st d in dom fn holds
fn . d = i |^ (d -' 1) ) implies for d, e being Element of NAT st d in dom fn & e in dom fn & d <> e holds
not fn . d,fn . e are_congruent_mod n )
assume A1: ( n > 1 & i,n are_coprime & len fn = order (i,n) & ( for d being Element of NAT st d in dom fn holds
fn . d = i |^ (d -' 1) ) ) ; :: thesis: for d, e being Element of NAT st d in dom fn & e in dom fn & d <> e holds
not fn . d,fn . e are_congruent_mod n
then A2: ( i <> 0 & n <> 0 ) by Th5;
A3: i gcd n = 1 by A1, INT_2:def 3;
assume ex d, e being Element of NAT st
( d in dom fn & e in dom fn & d <> e & fn . d,fn . e are_congruent_mod n ) ; :: thesis: contradiction
then consider d, e being Element of NAT such that
A4: ( d in dom fn & e in dom fn & d <> e & fn . d,fn . e are_congruent_mod n ) ;
A5: ( d >= 1 & d <= order (i,n) & e >= 1 & e <= order (i,n) ) by A4, A1, FINSEQ_3:25;
then (d -' 1) + 1 = (d + 1) -' 1 by NAT_D:38
.= (d + 1) - 1 by NAT_D:37
.= (d - 1) + 1 ;
then A6: d -' 1 = d - 1 ;
(e -' 1) + 1 = (e + 1) -' 1 by NAT_D:38, A5
.= (e + 1) - 1 by NAT_D:37
.= (e - 1) + 1 ;
then A7: ( d - 1 = d -' 1 & e - 1 = e -' 1 ) by A6;

per cases ( d > e or e > d ) by A4, XXREAL_0:1;

suppose d > e ; :: thesis: contradiction

then A8: e -' 1 < d -' 1 by A7, XREAL_1:9;
then consider k being Nat such that
A9: d -' 1 = (e -' 1) + k by NAT_1:10;
reconsider ll = (i |^ k) - 1 as Element of NAT by A2, NAT_1:21, NAT_1:14;
A10: (i |^ (d -' 1)) - (i |^ (e -' 1)) = ((i |^ (e -' 1)) * (i |^ k)) - ((i |^ (e -' 1)) * 1) by A9, NEWTON:8
.= (i |^ (e -' 1)) * ll ;
A11: (i |^ (e -' 1)) gcd n = 1 by A2, A3, NAT_4:10;
i |^ (d -' 1),fn . e are_congruent_mod n by A1, A4;
then i |^ (d -' 1),i |^ (e -' 1) are_congruent_mod n by A1, A4;
then n divides (i |^ (d -' 1)) - (i |^ (e -' 1)) by INT_2:15;
then n divides ll by A10, A11, WSIERP_1:30;
then i |^ k,1 are_congruent_mod n by INT_2:15;
then A12: (i |^ k) mod n = 1 mod n by NAT_D:64
.= 1 by A1, PEPIN:5 ;
A13: (d -' 1) - (e -' 1) > 0 by A8, XREAL_1:50;
A14: order (i,n) <= k by A13, A9, NAT_D:7, A1, A12, PEPIN:47;
d - e <= (order (i,n)) - 1 by A5, XREAL_1:13;
hence contradiction by A7, A9, A14, XXREAL_0:2, XREAL_1:146; :: thesis: verum

end;

suppose e > d ; :: thesis: contradiction

then A15: e -' 1 > d -' 1 by A7, XREAL_1:9;
then consider k being Nat such that
A16: e -' 1 = (d -' 1) + k by NAT_1:10;
reconsider ll = (i |^ k) - 1 as Element of NAT by A2, NAT_1:21, NAT_1:14;
A17: (i |^ (e -' 1)) - (i |^ (d -' 1)) = ((i |^ (d -' 1)) * (i |^ k)) - ((i |^ (d -' 1)) * 1) by A16, NEWTON:8
.= (i |^ (d -' 1)) * ll ;
A18: (i |^ (d -' 1)) gcd n = 1 by A2, A3, NAT_4:10;
i |^ (d -' 1),fn . e are_congruent_mod n by A1, A4;
then i |^ (d -' 1),i |^ (e -' 1) are_congruent_mod n by A1, A4;
then i |^ (e -' 1),i |^ (d -' 1) are_congruent_mod n by INT_1:14;
then n divides (i |^ (e -' 1)) - (i |^ (d -' 1)) by INT_2:15;
then n divides ll by A17, A18, WSIERP_1:30;
then i |^ k,1 are_congruent_mod n by INT_2:15;
then A19: (i |^ k) mod n = 1 mod n by NAT_D:64
.= 1 by A1, PEPIN:5 ;
A20: (e -' 1) - (d -' 1) > 0 by A15, XREAL_1:50;
A21: order (i,n) <= k by A16, A20, NAT_D:7, A1, A19, PEPIN:47;
e - d <= (order (i,n)) - 1 by A5, XREAL_1:13;
hence contradiction by A16, A21, A7, XXREAL_0:2, XREAL_1:146; :: thesis: verum

end;

end;