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 and

A2: len fp = m and

A3: for b being Nat st b in dom fp holds

fp . b in Class ((Cong m),(b -' 1)) ;

A4: for x, y being Integer st x in X & y in X & x <> y holds

not [x,y] in Cong m

a = b

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, A2, A4, FINSEQ_4:62; :: thesis: verum

( 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 and

A2: len fp = m and

A3: for b being Nat st b in dom fp holds

fp . b in Class ((Cong m),(b -' 1)) ;

A4: for x, y being Integer st x in X & y in X & x <> y holds

not [x,y] in Cong m

proof

for a, b being object st a in dom fp & b in dom fp & fp . a = fp . b holds
let x, y be Integer; :: thesis: ( x in X & y in X & x <> y implies not [x,y] in Cong m )

assume that

A5: x in X and

A6: y in X and

A7: x <> y ; :: thesis: not [x,y] in Cong m

consider a being object such that

A8: a in dom fp and

A9: x = fp . a by A1, A5, FUNCT_1:def 3;

reconsider a = a as Element of NAT by A8;

x in Class ((Cong m),(a -' 1)) by A3, A8, A9;

then [(a -' 1),x] in Cong m by EQREL_1:18;

then A10: a -' 1,x are_congruent_mod m by Def1;

consider b being object such that

A11: b in dom fp and

A12: y = fp . b by A1, A6, FUNCT_1:def 3;

reconsider b = b as Element of NAT by A11;

A13: b in Seg m by A2, A11, FINSEQ_1:def 3;

then A14: b >= 1 by FINSEQ_1:1;

y in Class ((Cong m),(b -' 1)) by A3, A11, A12;

then [(b -' 1),y] in Cong m by EQREL_1:18;

then b -' 1,y are_congruent_mod m by Def1;

then A15: y,b -' 1 are_congruent_mod m by INT_1:14;

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 A15, INT_1:15;

then a -' 1,b -' 1 are_congruent_mod m by A10, INT_1:15;

then A16: m divides (a -' 1) - (b -' 1) ;

A17: a in Seg m by A2, A8, FINSEQ_1:def 3;

then A18: a >= 1 by FINSEQ_1:1;

b <= m by A13, FINSEQ_1:1;

then a - b >= 1 - m by A18, XREAL_1:13;

then A19: a - b > - m by XREAL_1:145;

a <= m by A17, FINSEQ_1:1;

then a - b <= m - 1 by A14, XREAL_1:13;

then a - b < m by XREAL_1:147;

then |.(a - b).| < m by A19, SEQ_2:1;

then A20: |.(a - b).| < |.m.| by ABSVALUE:def 1;

A21: (a -' 1) - (b -' 1) = (a - 1) - (b -' 1) by A18, XREAL_1:233

.= (a - 1) - (b - 1) by A14, XREAL_1:233

.= a - b ;

end;assume that

A5: x in X and

A6: y in X and

A7: x <> y ; :: thesis: not [x,y] in Cong m

consider a being object such that

A8: a in dom fp and

A9: x = fp . a by A1, A5, FUNCT_1:def 3;

reconsider a = a as Element of NAT by A8;

x in Class ((Cong m),(a -' 1)) by A3, A8, A9;

then [(a -' 1),x] in Cong m by EQREL_1:18;

then A10: a -' 1,x are_congruent_mod m by Def1;

consider b being object such that

A11: b in dom fp and

A12: y = fp . b by A1, A6, FUNCT_1:def 3;

reconsider b = b as Element of NAT by A11;

A13: b in Seg m by A2, A11, FINSEQ_1:def 3;

then A14: b >= 1 by FINSEQ_1:1;

y in Class ((Cong m),(b -' 1)) by A3, A11, A12;

then [(b -' 1),y] in Cong m by EQREL_1:18;

then b -' 1,y are_congruent_mod m by Def1;

then A15: y,b -' 1 are_congruent_mod m by INT_1:14;

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 A15, INT_1:15;

then a -' 1,b -' 1 are_congruent_mod m by A10, INT_1:15;

then A16: m divides (a -' 1) - (b -' 1) ;

A17: a in Seg m by A2, A8, FINSEQ_1:def 3;

then A18: a >= 1 by FINSEQ_1:1;

b <= m by A13, FINSEQ_1:1;

then a - b >= 1 - m by A18, XREAL_1:13;

then A19: a - b > - m by XREAL_1:145;

a <= m by A17, FINSEQ_1:1;

then a - b <= m - 1 by A14, XREAL_1:13;

then a - b < m by XREAL_1:147;

then |.(a - b).| < m by A19, SEQ_2:1;

then A20: |.(a - b).| < |.m.| by ABSVALUE:def 1;

A21: (a -' 1) - (b -' 1) = (a - 1) - (b -' 1) by A18, XREAL_1:233

.= (a - 1) - (b - 1) by A14, XREAL_1:233

.= a - b ;

now :: thesis: not a <> b

hence
contradiction
by A7, A9, A12; :: thesis: verumassume
a <> b
; :: thesis: contradiction

then a - b <> 0 ;

hence contradiction by A16, A21, A20, Th6; :: thesis: verum

end;then a - b <> 0 ;

hence contradiction by A16, A21, A20, Th6; :: thesis: verum

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

A22: a in dom fp and

A23: b in dom fp and

A24: fp . a = fp . b ; :: thesis: a = b

reconsider a = a, b = b as Element of NAT by A22, A23;

A25: b in Seg m by A2, A23, FINSEQ_1:def 3;

then A26: b >= 1 by FINSEQ_1:1;

reconsider l = fp . a, ll = fp . b as Element of INT by A22, A23, FINSEQ_2:11;

fp . b in Class ((Cong m),(b -' 1)) by A3, A23;

then [(b -' 1),(fp . b)] in Cong m by EQREL_1:18;

then b -' 1,ll are_congruent_mod m by Def1;

then A27: l,b -' 1 are_congruent_mod m by A24, INT_1:14;

A28: a in Seg m by A2, A22, FINSEQ_1:def 3;

then A29: a >= 1 by FINSEQ_1:1;

then A30: (a -' 1) - (b -' 1) = (a - 1) - (b -' 1) by XREAL_1:233

.= (a - 1) - (b - 1) by A26, XREAL_1:233

.= a - b ;

b <= m by A25, FINSEQ_1:1;

then a - b >= 1 - m by A29, XREAL_1:13;

then A31: a - b > - m by XREAL_1:145;

a <= m by A28, FINSEQ_1:1;

then a - b <= m - 1 by A26, XREAL_1:13;

then a - b < m by XREAL_1:147;

then |.(a - b).| < m by A31, SEQ_2:1;

then A32: |.(a - b).| < |.m.| by ABSVALUE:def 1;

fp . a in Class ((Cong m),(a -' 1)) by A3, A22;

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 A27, INT_1:15;

then A33: m divides a - b by A30;

end;assume that

A22: a in dom fp and

A23: b in dom fp and

A24: fp . a = fp . b ; :: thesis: a = b

reconsider a = a, b = b as Element of NAT by A22, A23;

A25: b in Seg m by A2, A23, FINSEQ_1:def 3;

then A26: b >= 1 by FINSEQ_1:1;

reconsider l = fp . a, ll = fp . b as Element of INT by A22, A23, FINSEQ_2:11;

fp . b in Class ((Cong m),(b -' 1)) by A3, A23;

then [(b -' 1),(fp . b)] in Cong m by EQREL_1:18;

then b -' 1,ll are_congruent_mod m by Def1;

then A27: l,b -' 1 are_congruent_mod m by A24, INT_1:14;

A28: a in Seg m by A2, A22, FINSEQ_1:def 3;

then A29: a >= 1 by FINSEQ_1:1;

then A30: (a -' 1) - (b -' 1) = (a - 1) - (b -' 1) by XREAL_1:233

.= (a - 1) - (b - 1) by A26, XREAL_1:233

.= a - b ;

b <= m by A25, FINSEQ_1:1;

then a - b >= 1 - m by A29, XREAL_1:13;

then A31: a - b > - m by XREAL_1:145;

a <= m by A28, FINSEQ_1:1;

then a - b <= m - 1 by A26, XREAL_1:13;

then a - b < m by XREAL_1:147;

then |.(a - b).| < m by A31, SEQ_2:1;

then A32: |.(a - b).| < |.m.| by ABSVALUE:def 1;

fp . a in Class ((Cong m),(a -' 1)) by A3, A22;

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 A27, INT_1:15;

then A33: m divides a - b by A30;

now :: thesis: not a <> b

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

then a - b <> 0 ;

hence contradiction by A33, A32, Th6; :: thesis: verum

end;then a - b <> 0 ;

hence contradiction by A33, A32, Th6; :: thesis: verum

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, A2, A4, FINSEQ_4:62; :: thesis: verum