let m be Element of NAT ; :: thesis: for X being finite Subset of INT st card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m ) holds
X is_CRS_of m
let X be finite Subset of INT ; :: 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 ) implies X is_CRS_of m )
assume A1: ( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m ) ) ; :: thesis: X is_CRS_of m

per cases ( X is empty or not X is empty ) ;

suppose X is empty ; :: thesis: X is_CRS_of m

hence X is_CRS_of m by A1, Th50, CARD_1:47; :: thesis: verum

end;

suppose not X is empty ; :: thesis: X is_CRS_of m

then reconsider X = X as non empty finite Subset of INT ;
A2: X <> {} ;
then A3: m <> 0 by A1;
then A4: m > 0 ;
defpred S₁[ Nat, set ] means $2 in Class (Cong m),($1 -' 1);
A5: for a being Nat st a in Seg m holds
ex y being Element of X st S₁[a,y]

proof

let a be Nat; :: thesis: ( a in Seg m implies ex y being Element of X st S₁[a,y] )
assume A6: a in Seg m ; :: thesis: ex y being Element of X st S₁[a,y]
consider fp being FinSequence such that
A7: ( len fp = m & ( for b being Element of NAT st b in dom fp holds
fp . b in X ) & fp is one-to-one ) by A1, Th51;
for b being Nat st b in dom fp holds
fp . b in X by A7;
then reconsider fp = fp as FinSequence of X by FINSEQ_2:14;
defpred S₂[ Nat, set ] means fp . $1 in Class (Cong m),$2;
set Y = Segm m;
A8: for c being Element of NAT st c in Seg m holds
ex r being Element of Segm m st S₂[c,r]

proof

let c be Element of NAT ; :: thesis: ( c in Seg m implies ex r being Element of Segm m st S₂[c,r] )
assume c in Seg m ; :: thesis: ex r being Element of Segm m st S₂[c,r]
consider q, r being Integer such that
A9: ( fp . c = (m * q) + r & r >= 0 & r < m ) by A4, Th13;
(fp . c) mod m = r mod m by A9, INT_3:8;
then r,fp . c are_congruent_mod m by A3, INT_3:12;
then A10: [r,(fp . c)] in Cong m by Def1;
reconsider r = r as Element of NAT by A9, INT_1:16;
reconsider r = r as Element of Segm m by A9, NAT_1:45;
take r ; :: thesis: S₂[c,r]
thus S₂[c,r] by A10, EQREL_1:26; :: thesis: verum

end;

reconsider Y = Segm m as non empty set by A1, A2;
A11: for c being Nat st c in Seg m holds
ex r being Element of Y st S₂[c,r] by A8;
consider fr being FinSequence of Y such that
A12: ( dom fr = Seg m & ( for c being Nat st c in Seg m holds
S₂[c,fr . c] ) ) from FINSEQ_1:sch 5(A11);
for x1, x2 being set st x1 in dom fr & x2 in dom fr & fr . x1 = fr . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in dom fr & x2 in dom fr & fr . x1 = fr . x2 implies x1 = x2 )
assume A13: ( x1 in dom fr & x2 in dom fr & fr . x1 = fr . x2 ) ; :: thesis: x1 = x2
( fp . x1 in Class (Cong m),(fr . x1) & fp . x2 in Class (Cong m),(fr . x1) ) by A12, A13;
then A14: [(fp . x1),(fp . x2)] in Cong m by EQREL_1:30;
assume A15: x1 <> x2 ; :: thesis: contradiction
reconsider x1 = x1, x2 = x2 as Element of NAT by A13;
A16: ( x1 in dom fp & x2 in dom fp ) by A7, A12, A13, FINSEQ_1:def 3;
then A17: ( fp . x1 in X & fp . x2 in X ) by FINSEQ_2:13;
fp . x1 <> fp . x2 by A7, A15, A16, FUNCT_1:def 8;
hence contradiction by A1, A14, A17; :: thesis: verum

end;

then fr is one-to-one by FUNCT_1:def 8;
then A18: card (rng fr) = len fr by FINSEQ_4:77
.= m by A12, FINSEQ_1:def 3 ;
reconsider Y = Y as finite set ;
m = { l where l is Element of NAT : l < m } by AXIOMS:30;
then Y is_CRS_of m by Th48;
then card Y = m by Th49;
then A19: rng fr = Y by A18, CARD_FIN:1;
A20: ( a >= 1 & a <= m ) by A6, FINSEQ_1:3;
then ( a - 1 >= 0 & a - 1 < m ) by XREAL_1:50, XREAL_1:149;
then ( a -' 1 >= 0 & a -' 1 < m ) by A20, XREAL_1:235;
then a -' 1 in Y by NAT_1:45;
then consider w being set such that
A21: ( w in dom fr & fr . w = a -' 1 ) by A19, FUNCT_1:def 5;
reconsider w = w as Element of NAT by A21;
w in dom fp by A7, A12, A21, FINSEQ_1:def 3;
then reconsider y = fp . w as Element of X by FINSEQ_2:13;
take y ; :: thesis: S₁[a,y]
thus S₁[a,y] by A12, A21; :: thesis: verum

end;

consider fp being FinSequence of X such that
A22: ( dom fp = Seg m & ( for a being Nat st a in Seg m holds
S₁[a,fp . a] ) ) from FINSEQ_1:sch 5(A5);
A23: len fp = m by A22, FINSEQ_1:def 3;
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 A24: ( 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 A24, FINSEQ_2:13;
( fp . a in Class (Cong m),(a -' 1) & fp . b in Class (Cong m),(b -' 1) ) by A22, A24;
then ( [(a -' 1),(fp . a)] in Cong m & [(b -' 1),(fp . b)] in Cong m ) by EQREL_1:26;
then A25: ( 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 A24, INT_1:35;
then A26: a -' 1,b -' 1 are_congruent_mod m by A25, INT_1:36;
A27: ( a >= 1 & a <= m & b >= 1 & b <= m ) by A22, A24, FINSEQ_1:3;
then (a -' 1) - (b -' 1) = (a - 1) - (b -' 1) by XREAL_1:235
.= (a - 1) - (b - 1) by A27, XREAL_1:235
.= a - b ;
then A28: m divides a - b by A26, INT_2:19;
( a - b <= m - 1 & a - b >= 1 - m ) by A27, 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 A29: abs (a - b) < abs m by ABSVALUE:def 1;

now

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

end;

hence a = b ; :: thesis: verum

end;

then fp is one-to-one by FUNCT_1:def 8;
then A30: card X = card (rng fp) by A1, A23, FINSEQ_4:77;
rng fp c= X by FINSEQ_1:def 4;
then X = rng fp by A30, CARD_FIN:1;
hence X is_CRS_of m by A22, A23, Def2; :: thesis: verum

end;

end;