let m be Element of NAT ; :: thesis: for X being finite set st X is_CRS_of m holds
( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m ) )
let X be finite set ; :: thesis: ( X is_CRS_of m implies ( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m ) ) )
assume X is_CRS_of m ; :: thesis: ( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m ) )
then consider fp being FinSequence of INT such that
A1: ( X = rng fp & len fp = m & ( for b being Nat st b in dom fp holds
fp . b in Class (Cong m),(b -' 1) ) ) by Def2;
for a, b being set st a in dom fp & b in dom fp & fp . a = fp . b holds
a = b

proof

let a, b be set ; :: thesis: ( a in dom fp & b in dom fp & fp . a = fp . b implies a = b )
assume A2: ( a in dom fp & b in dom fp & fp . a = fp . b ) ; :: thesis: a = b
then reconsider a = a, b = b as Element of NAT ;
reconsider l = fp . a, ll = fp . b as Element of INT by A2, FINSEQ_2:13;
( fp . a in Class (Cong m),(a -' 1) & fp . b in Class (Cong m),(b -' 1) ) by A1, A2;
then ( [(a -' 1),(fp . a)] in Cong m & [(b -' 1),(fp . b)] in Cong m ) by EQREL_1:26;
then A3: ( a -' 1,l are_congruent_mod m & b -' 1,ll are_congruent_mod m ) by Def1;
then l,b -' 1 are_congruent_mod m by A2, INT_1:35;
then A4: a -' 1,b -' 1 are_congruent_mod m by A3, INT_1:36;
( a in Seg m & b in Seg m ) by A1, A2, FINSEQ_1:def 3;
then A5: ( a >= 1 & a <= m & b >= 1 & b <= m ) by FINSEQ_1:3;
then (a -' 1) - (b -' 1) = (a - 1) - (b -' 1) by XREAL_1:235
.= (a - 1) - (b - 1) by A5, XREAL_1:235
.= a - b ;
then A6: m divides a - b by A4, INT_2:19;
( a - b <= m - 1 & a - b >= 1 - m ) by A5, XREAL_1:15;
then ( a - b < m & a - b > - m ) by XREAL_1:147, XREAL_1:149;
then abs (a - b) < m by SEQ_2:9;
then A7: abs (a - b) < abs m by ABSVALUE:def 1;

now

assume a <> b ; :: thesis: contradiction
then a - b <> 0 ;
hence contradiction by A6, A7, Th6; :: thesis: verum

end;

hence a = b ; :: thesis: verum

end;

then A8: fp is one-to-one by FUNCT_1:def 8;
for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m

proof

let x, y be Integer; :: thesis: ( x in X & y in X & x <> y implies not [x,y] in Cong m )
assume A9: ( x in X & y in X & x <> y ) ; :: thesis: not [x,y] in Cong m
then consider a being set such that
A10: ( a in dom fp & x = fp . a ) by A1, FUNCT_1:def 5;
reconsider a = a as Element of NAT by A10;
x in Class (Cong m),(a -' 1) by A1, A10;
then [(a -' 1),x] in Cong m by EQREL_1:26;
then A11: a -' 1,x are_congruent_mod m by Def1;
consider b being set such that
A12: ( b in dom fp & y = fp . b ) by A1, A9, FUNCT_1:def 5;
reconsider b = b as Element of NAT by A12;
y in Class (Cong m),(b -' 1) by A1, A12;
then [(b -' 1),y] in Cong m by EQREL_1:26;
then b -' 1,y are_congruent_mod m by Def1;
then A13: y,b -' 1 are_congruent_mod m by INT_1:35;
assume [x,y] in Cong m ; :: thesis: contradiction
then x,y are_congruent_mod m by Def1;
then x,b -' 1 are_congruent_mod m by A13, INT_1:36;
then a -' 1,b -' 1 are_congruent_mod m by A11, INT_1:36;
then A14: m divides (a -' 1) - (b -' 1) by INT_2:19;
( a in Seg m & b in Seg m ) by A1, A10, A12, FINSEQ_1:def 3;
then A15: ( a >= 1 & a <= m & b >= 1 & b <= m ) by FINSEQ_1:3;
then A16: (a -' 1) - (b -' 1) = (a - 1) - (b -' 1) by XREAL_1:235
.= (a - 1) - (b - 1) by A15, XREAL_1:235
.= a - b ;
( a - b <= m - 1 & a - b >= 1 - m ) by A15, XREAL_1:15;
then ( a - b < m & a - b > - m ) by XREAL_1:147, XREAL_1:149;
then abs (a - b) < m by SEQ_2:9;
then A17: abs (a - b) < abs m by ABSVALUE:def 1;

now

assume a <> b ; :: thesis: contradiction
then a - b <> 0 ;
hence contradiction by A14, A16, A17, Th6; :: thesis: verum

end;

hence contradiction by A9, A10, A12; :: thesis: verum

end;

hence ( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m ) ) by A1, A8, FINSEQ_4:77; :: thesis: verum