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 that
A1: card X = m and
A2: 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; :: 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 ;
defpred S₁[ Nat, set ] means $2 in Class ((Cong m),($1 -' 1));
A3: X <> {} ;
A4: for a being Nat st a in Seg m holds
ex y being Element of X st S₁[a,y]

proof

set Y = Segm m;
let a be Nat; :: thesis: ( a in Seg m implies ex y being Element of X st S₁[a,y] )
assume A5: a in Seg m ; :: thesis: ex y being Element of X st S₁[a,y]
a <= m by A5, FINSEQ_1:1;
then A6: a - 1 < m by XREAL_1:147;
consider fp being FinSequence such that
A7: len fp = m and
A8: for b being Element of NAT st b in dom fp holds
fp . b in X and
A9: fp is one-to-one by A1, Th51;
for b being Nat st b in dom fp holds
fp . b in X by A8;
then reconsider fp = fp as FinSequence of X by FINSEQ_2:12;
defpred S₂[ Nat, set ] means fp . $1 in Class ((Cong m),$2);
A10: 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
A11: fp . c = (m * q) + r and
A12: r >= 0 and
A13: r < m by A1, Th13;
(fp . c) mod m = r mod m by A11, NAT_D:61;
then r,fp . c are_congruent_mod m by A1, NAT_D:64;
then A14: [r,(fp . c)] in Cong m by Def1;
reconsider r = r as Element of NAT by A12, INT_1:3;
reconsider r = r as Element of Segm m by A13, NAT_1:44;
take r ; :: thesis: S₂[c,r]
thus S₂[c,r] by A14, EQREL_1:18; :: thesis: verum

end;

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

proof

let x1, x2 be object ; :: thesis: ( x1 in dom fr & x2 in dom fr & fr . x1 = fr . x2 implies x1 = x2 )
assume that
A17: x1 in dom fr and
A18: x2 in dom fr and
A19: fr . x1 = fr . x2 ; :: thesis: x1 = x2
( fp . x1 in Class ((Cong m),(fr . x1)) & fp . x2 in Class ((Cong m),(fr . x1)) ) by A16, A17, A18, A19;
then A20: [(fp . x1),(fp . x2)] in Cong m by EQREL_1:22;
assume A21: x1 <> x2 ; :: thesis: contradiction
reconsider x1 = x1, x2 = x2 as Element of NAT by A17, A18;
A22: x1 in dom fp by A7, A16, A17, FINSEQ_1:def 3;
then A23: fp . x1 in X by FINSEQ_2:11;
A24: x2 in dom fp by A7, A16, A18, FINSEQ_1:def 3;
then A25: fp . x2 in X by FINSEQ_2:11;
fp . x1 <> fp . x2 by A9, A21, A22, A24;
hence contradiction by A2, A20, A23, A25; :: thesis: verum

end;

then fr is one-to-one ;
then A26: card (rng fr) = len fr by FINSEQ_4:62
.= m by A16, FINSEQ_1:def 3 ;
reconsider Y = Y as finite set ;
a >= 1 by A5, FINSEQ_1:1;
then a -' 1 < m by A6, XREAL_1:233;
then A27: a -' 1 in Y by NAT_1:44;
card Y = m ;
then rng fr = Y by A26, CARD_2:102;
then consider w being object such that
A28: w in dom fr and
A29: fr . w = a -' 1 by A27, FUNCT_1:def 3;
reconsider w = w as Element of NAT by A28;
w in dom fp by A7, A16, A28, FINSEQ_1:def 3;
then reconsider y = fp . w as Element of X by FINSEQ_2:11;
take y ; :: thesis: S₁[a,y]
thus S₁[a,y] by A16, A28, A29; :: thesis: verum

end;

consider fp being FinSequence of X such that
A30: ( dom fp = Seg m & ( for a being Nat st a in Seg m holds
S₁[a,fp . a] ) ) from FINSEQ_1:sch 5(A4);
A31: rng fp c= X by FINSEQ_1:def 4;
A32: len fp = m by A30, FINSEQ_1:def 3;
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 that
A33: a in dom fp and
A34: b in dom fp and
A35: fp . a = fp . b ; :: thesis: a = b
reconsider a = a, b = b as Element of NAT by A33, A34;
A36: b >= 1 by A30, A34, FINSEQ_1:1;
A37: a >= 1 by A30, A33, FINSEQ_1:1;
then A38: (a -' 1) - (b -' 1) = (a - 1) - (b -' 1) by XREAL_1:233
.= (a - 1) - (b - 1) by A36, XREAL_1:233
.= a - b ;
reconsider l = fp . a, ll = fp . b as Element of INT by A33, A34, FINSEQ_2:11;
fp . b in Class ((Cong m),(b -' 1)) by A30, A34;
then [(b -' 1),(fp . b)] in Cong m by EQREL_1:18;
then b -' 1,ll are_congruent_mod m by Def1;
then A39: l,b -' 1 are_congruent_mod m by A35, INT_1:14;
b <= m by A30, A34, FINSEQ_1:1;
then a - b >= 1 - m by A37, XREAL_1:13;
then A40: a - b > - m by XREAL_1:145;
a <= m by A30, A33, FINSEQ_1:1;
then a - b <= m - 1 by A36, XREAL_1:13;
then a - b < m by XREAL_1:147;
then |.(a - b).| < m by A40, SEQ_2:1;
then A41: |.(a - b).| < |.m.| by ABSVALUE:def 1;
fp . a in Class ((Cong m),(a -' 1)) by A30, A33;
then [(a -' 1),(fp . a)] in Cong m by EQREL_1:18;
then a -' 1,l are_congruent_mod m by Def1;
then a -' 1,b -' 1 are_congruent_mod m by A39, INT_1:15;
then A42: m divides a - b by A38;

now :: thesis: not a <> b

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

end;

hence a = b ; :: thesis: verum

end;

then fp is one-to-one ;
then card X = card (rng fp) by A1, A32, FINSEQ_4:62;
then X = rng fp by A31, CARD_2:102;
hence X is_CRS_of m by A30, A32; :: thesis: verum

end;

end;