let m be Nat; :: thesis:
let X be finite Subset of INT; :: thesis:
assume A1: ( 1 < m & card X = Euler m & ( for x, y being Integer st x in X & y in X & x <> y holds
not x,y are_congruent_mod m ) & ( for x being Integer st x in X holds
x,m are_coprime ) ) ; :: thesis:
then card X <> 0 by PEPIN:42;
then reconsider X = X as non empty finite Subset of INT ;
set Y = RelPrimes m;
A2: RelPrimes m c= Seg m by Th1;
reconsider Y = RelPrimes m as finite set ;
m gcd 1 = 1 by NEWTON:51;
then m,1 are_coprime by INT_2:def 3;
then 1 in Y by A1;
then reconsider Y = Y as non empty finite set ;
reconsider Y = Y as non empty finite Subset of INT by NUMBERS:17, XBOOLE_1:1;
A3: Y is_RRS_of m by Th22;
defpred S₁[ Nat, set ] means $2 in Class ((Cong m),((Sgm Y) . $1));
A4: for a being Nat st a in Seg (Euler m) holds
ex y being Element of X st S₁[a,y]

let a be Nat; :: thesis:
assume A5: a in Seg (Euler m) ; :: thesis:
consider fp being FinSequence such that
A6: ( len fp = Euler m & ( for d being Element of NAT st d in dom fp holds
fp . d in X ) & fp is one-to-one ) by A1, INT_4:51;
for d being Nat st d in dom fp holds
fp . d in X by A6;
then reconsider fp = fp as FinSequence of X by FINSEQ_2:12;
A7: card (rng fp) = card X by A1, A6, FINSEQ_4:62;
rng fp c= X by FINSEQ_1:def 4;
then A8: rng fp = X by A7, CARD_2:102;
defpred S₂[ Nat, set ] means fp . $1 in Class ((Cong m),$2);
A9: for c being Nat st c in Seg (Euler m) holds
ex r being Element of Y st S₂[c,r]

let c be Nat; :: thesis:
assume c in Seg (Euler m) ; :: thesis:
then c in dom fp by A6, FINSEQ_1:def 3;
then A10: fp . c,m are_coprime by A1, A6;
set r = (fp . c) mod m;
A11: (fp . c) mod m = ((((fp . c) div m) * m) + ((fp . c) mod m)) mod m by A1, INT_1:59
.= ((fp . c) mod m) mod m by EULER_1:12 ;
then fp . c,(fp . c) mod m are_congruent_mod m by A1, NAT_D:64;
then A12: ((fp . c) mod m) gcd m = (fp . c) gcd m by WSIERP_1:43
.= 1 by A10, INT_2:def 3 ;
then A13: (fp . c) mod m,m are_coprime by INT_2:def 3;
reconsider r = (fp . c) mod m as Element of NAT by INT_1:3, INT_1:57;
reconsider zz = 0 , j = 1 as Real ;

end;

end;

consider fr being FinSequence of Y such that
A16: ( dom fr = Seg (Euler m) & ( for c being Nat st c in Seg (Euler m) holds
S₂[c,fr . c] ) ) from FINSEQ_1:sch 5(A9);
for x1, x2 being object st x1 in dom fr & x2 in dom fr & fr . x1 = fr . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis:
assume A17: ( x1 in dom fr & x2 in dom fr & fr . x1 = fr . x2 ) ; :: thesis:
then reconsider x1 = x1, x2 = x2 as Element of NAT ;
( fp . x1 in Class ((Cong m),(fr . x1)) & fp . x2 in Class ((Cong m),(fr . x2)) ) by A17, A16;
then ( [(fr . x1),(fp . x1)] in Cong m & [(fr . x2),(fp . x2)] in Cong m ) by EQREL_1:18;
then ( fr . x1,fp . x1 are_congruent_mod m & fr . x2,fp . x2 are_congruent_mod m ) by INT_4:def 1;
then A18: fp . x1,fp . x2 are_congruent_mod m by A17, PEPIN:40;
A19: ( x1 in dom fp & x2 in dom fp ) by A17, A6, A16, FINSEQ_1:def 3;
then ( fp . x1 in X & fp . x2 in X ) by A8, FUNCT_1:def 3;
then fp . x1 = fp . x2 by A1, A18;
hence x1 = x2 by A19, A6, FUNCT_1:def 4; :: thesis:

end;

end;

consider f being FinSequence of X such that
A23: ( dom f = Seg (Euler m) & ( for a being Nat st a in Seg (Euler m) holds
S₁[a,f . a] ) ) from FINSEQ_1:sch 5(A4);
A24: len f = Euler m by A23, FINSEQ_1:def 3;
for a, b being object st a in dom f & b in dom f & f . a = f . b holds
a = b

let a, b be object ; :: thesis:
assume A25: ( a in dom f & b in dom f & f . a = f . b ) ; :: thesis:
then reconsider a = a, b = b as Element of NAT ;
( f . a in Class ((Cong m),((Sgm Y) . a)) & f . b in Class ((Cong m),((Sgm Y) . b)) ) by A25, A23;
then ( [((Sgm Y) . a),(f . a)] in Cong m & [((Sgm Y) . b),(f . b)] in Cong m ) by EQREL_1:18;
then A26: ( (Sgm Y) . a,f . a are_congruent_mod m & (Sgm Y) . b,f . b are_congruent_mod m ) by INT_4:def 1;
then f . b,(Sgm Y) . b are_congruent_mod m by INT_1:14;
then A27: (Sgm Y) . a,(Sgm Y) . b are_congruent_mod m by A26, A25, INT_1:15;

end;

hence a = b ; :: thesis:

end;