let m be Element of NAT ; :: thesis:
let a be Integer; :: thesis:
let X be finite Subset of INT; :: thesis:
assume that
A1: a,m are_coprime and
A2: X is_CRS_of m ; :: thesis:
A3: card X = m by A2, Th49;
A4: a ** X c= INT by Lm2;

suppose A5: a = 0 ; :: thesis:

then a gcd m = |.m.| by WSIERP_1:8
.= m by ABSVALUE:def 1 ;
then A6: m = 1 by A1, INT_2:def 3;
then ex x being object st X = {x} by A3, CARD_2:42;
then A7: a ** X = {0} by A5, Th4;
A8: for x, y being Integer st x in a ** X & y in a ** X & x <> y holds
not [x,y] in Cong m

let x, y be Integer; :: thesis:
assume that
A9: x in a ** X and
A10: ( y in a ** X & x <> y ) ; :: thesis:
assume [x,y] in Cong m ; :: thesis:
x = 0 by A7, A9, TARSKI:def 1;
hence contradiction by A7, A10, TARSKI:def 1; :: thesis:

end;

card (a ** X) = m by A6, A7, CARD_2:42;
hence a ** X is_CRS_of m by A4, A8, Th52; :: thesis:

end;

suppose A11: a <> 0 ; :: thesis:

A12: for x, y being Integer st x in a ** X & y in a ** X & x <> y holds
not [x,y] in Cong m

let x, y be Integer; :: thesis:
assume that
A13: x in a ** X and
A14: y in a ** X and
A15: x <> y ; :: thesis:
consider y1 being Integer such that
A16: y1 in X and
A17: y = a * y1 by A14, Lm3;
consider x1 being Integer such that
A18: x1 in X and
A19: x = a * x1 by A13, Lm3;
not [x1,y1] in Cong m by A2, A15, A18, A19, A16, A17, Th49;
then A20: not x1,y1 are_congruent_mod m by Def1;
assume [x,y] in Cong m ; :: thesis:
then a * x1,a * y1 are_congruent_mod m by A19, A17, Def1;
hence contradiction by A1, A20, Th9; :: thesis:

end;

card (a ** X) = m by A3, A11, Th5;
hence a ** X is_CRS_of m by A4, A12, Th52; :: thesis:

end;

end;