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

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 )
;

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_{1}[ 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_{1}[a,y]

A30: ( dom fp = Seg m & ( for a being Nat st a in Seg m holds

S_{1}[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

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;defpred S

A3: X <> {} ;

A4: for a being Nat st a in Seg m holds

ex y being Element of X st S

proof

consider fp being FinSequence of X such that
set Y = Segm m;

let a be Nat; :: thesis: ( a in Seg m implies ex y being Element of X st S_{1}[a,y] )

assume A5: a in Seg m ; :: thesis: ex y being Element of X st S_{1}[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_{2}[ 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_{2}[c,r]

A15: for c being Nat st c in Seg m holds

ex r being Element of Y st S_{2}[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_{2}[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

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_{1}[a,y]

thus S_{1}[a,y]
by A16, A28, A29; :: thesis: verum

end;let a be Nat; :: thesis: ( a in Seg m implies ex y being Element of X st S

assume A5: a in Seg m ; :: thesis: ex y being Element of X st S

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

A10: for c being Element of NAT st c in Seg m holds

ex r being Element of Segm m st S

proof

reconsider Y = Segm m as non empty set by A1, A3;
let c be Element of NAT ; :: thesis: ( c in Seg m implies ex r being Element of Segm m st S_{2}[c,r] )

assume c in Seg m ; :: thesis: ex r being Element of Segm m st S_{2}[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_{2}[c,r]

thus S_{2}[c,r]
by A14, EQREL_1:18; :: thesis: verum

end;assume c in Seg m ; :: thesis: ex r being Element of Segm m st S

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

thus S

A15: for c being Nat st c in Seg m holds

ex r being Element of Y st S

consider fr being FinSequence of Y such that

A16: ( dom fr = Seg m & ( for c being Nat st c in Seg m holds

S

for x1, x2 being object st x1 in dom fr & x2 in dom fr & fr . x1 = fr . x2 holds

x1 = x2

proof

then
fr is one-to-one
;
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;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

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

thus S

A30: ( dom fp = Seg m & ( for a being Nat st a in Seg m holds

S

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

then
fp is one-to-one
;
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;

end;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

hence
a = b
; :: thesis: verumassume
a <> b
; :: thesis: contradiction

then a - b <> 0 ;

hence contradiction by A42, A41, Th6; :: thesis: verum

end;then a - b <> 0 ;

hence contradiction by A42, A41, Th6; :: thesis: verum

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