let m be Nat; :: thesis: for X being finite set st X is_RRS_of m holds
( 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 ) )
let X be finite set ; :: thesis: ( X is_RRS_of m implies ( 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 ) ) )
assume X is_RRS_of m ; :: thesis: ( 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 ) )
then consider fp being FinSequence of INT such that
A1: ( len fp = len (Sgm (RelPrimes m)) & ( for d being Element of NAT st d in dom fp holds
fp . d in Class ((Cong m),((Sgm (RelPrimes m)) . d)) ) & X = rng fp ) ;
A2: dom fp = dom (Sgm (RelPrimes m)) by A1, FINSEQ_3:29;
for a, b being object st a in dom fp & b in dom fp & fp . a = fp . b holds
a = b

proof

let a, b be object ; :: thesis: ( a in dom fp & b in dom fp & fp . a = fp . b implies a = b )
assume A3: ( a in dom fp & b in dom fp & fp . a = fp . b ) ; :: thesis: a = b
reconsider a = a, b = b as Element of NAT by A3;
reconsider l = fp . a, ll = fp . b as Element of INT by A3, FINSEQ_2:11;
( l in Class ((Cong m),((Sgm (RelPrimes m)) . a)) & ll in Class ((Cong m),((Sgm (RelPrimes m)) . b)) ) by A1, A3;
then ( [((Sgm (RelPrimes m)) . a),l] in Cong m & [((Sgm (RelPrimes m)) . b),ll] in Cong m ) by EQREL_1:18;
then A4: ( (Sgm (RelPrimes m)) . a,l are_congruent_mod m & (Sgm (RelPrimes m)) . b,ll are_congruent_mod m ) by INT_4:def 1;
then l,(Sgm (RelPrimes m)) . b are_congruent_mod m by A3, INT_1:14;
hence a = b by Th23, A3, A2, A4, INT_1:15; :: thesis: verum

end;

then A5: fp is one-to-one by FUNCT_1:def 4;
A7: card X = len (Sgm (RelPrimes m)) by A1, FINSEQ_4:62, A5
.= Euler m by FINSEQ_3:39 ;
A8: for x, y being Integer st x in X & y in X & x <> y holds
not x,y are_congruent_mod m

proof

let x, y be Integer; :: thesis: ( x in X & y in X & x <> y implies not x,y are_congruent_mod m )
assume A9: ( x in X & y in X & x <> y ) ; :: thesis: not x,y are_congruent_mod m
then consider d being Nat such that
A10: ( d in dom fp & fp . d = x ) by A1, FINSEQ_2:10;
consider e being Nat such that
A11: ( e in dom fp & fp . e = y ) by A1, A9, FINSEQ_2:10;
A12: ( d in dom (Sgm (RelPrimes m)) & e in dom (Sgm (RelPrimes m)) ) by A10, A11, A1, FINSEQ_3:29;
reconsider d = d, e = e as Element of NAT by A10, A11;
( fp . d in Class ((Cong m),((Sgm (RelPrimes m)) . d)) & fp . e in Class ((Cong m),((Sgm (RelPrimes m)) . e)) ) by A10, A11, A1;
then ( [((Sgm (RelPrimes m)) . d),(fp . d)] in Cong m & [((Sgm (RelPrimes m)) . e),(fp . e)] in Cong m ) by EQREL_1:18;
then A13: ( (Sgm (RelPrimes m)) . d,fp . d are_congruent_mod m & (Sgm (RelPrimes m)) . e,fp . e are_congruent_mod m ) by INT_4:def 1;

now :: thesis: not fp . d,fp . e are_congruent_mod m

assume fp . d,fp . e are_congruent_mod m ; :: thesis: contradiction
then (Sgm (RelPrimes m)) . d,fp . e are_congruent_mod m by A13, INT_1:15;
then fp . e,(Sgm (RelPrimes m)) . d are_congruent_mod m by INT_1:14;
hence contradiction by A12, A10, A11, A9, Th23, A13, INT_1:15; :: thesis: verum

end;

hence not x,y are_congruent_mod m by A10, A11; :: thesis: verum

end;

for x being Integer st x in X holds
x,m are_coprime

proof

let x be Integer; :: thesis: ( x in X implies x,m are_coprime )
assume x in X ; :: thesis: x,m are_coprime
then consider d being Nat such that
A14: ( d in dom fp & fp . d = x ) by A1, FINSEQ_2:10;
reconsider d = d as Element of NAT by A14;
fp . d in Class ((Cong m),((Sgm (RelPrimes m)) . d)) by A1, A14;
then [((Sgm (RelPrimes m)) . d),(fp . d)] in Cong m by EQREL_1:18;
then (Sgm (RelPrimes m)) . d,fp . d are_congruent_mod m by INT_4:def 1;
then A15: ((Sgm (RelPrimes m)) . d) gcd m = (fp . d) gcd m by WSIERP_1:43;
rng (Sgm (RelPrimes m)) = RelPrimes m by FINSEQ_1:def 14;
then (Sgm (RelPrimes m)) . d in RelPrimes m by A2, A14, FUNCT_1:def 3;
then consider k being Element of NAT such that
A16: ( (Sgm (RelPrimes m)) . d = k & m,k are_coprime & k >= 1 & k <= m ) ;
(fp . d) gcd m = 1 by A15, A16, INT_2:def 3;
hence x,m are_coprime by A14, INT_2:def 3; :: thesis: verum

end;

hence ( 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 ) ) by A7, A8; :: thesis: verum