let m be Nat; :: thesis: for X being finite Subset of INT
for a being Integer st m > 1 & a,m are_coprime & X is_RRS_of m holds
a ** X is_RRS_of m
let X be finite Subset of INT; :: thesis: for a being Integer st m > 1 & a,m are_coprime & X is_RRS_of m holds
a ** X is_RRS_of m
let a be Integer; :: thesis: ( m > 1 & a,m are_coprime & X is_RRS_of m implies a ** X is_RRS_of m )
assume A1: ( m > 1 & a,m are_coprime & X is_RRS_of m ) ; :: thesis: a ** X is_RRS_of m
then A2: ( card X = Euler m & ( for x, y being Integer st x in X & y in X & x <> y holds
not x,y are_congruent_mod m ) & ( for x being Integer st x in X holds
x,m are_coprime ) ) by Th24;
A3: a ** X c= INT by INT_1:def 2;
a <> 0 by A1, Th5;
then A4: card (a ** X) = Euler m by A2, INT_4:5;
A5: for x, y being Integer st x in a ** X & y in a ** X & x <> y holds
not x,y are_congruent_mod m

proof

let x, y be Integer; :: thesis: ( x in a ** X & y in a ** X & x <> y implies not x,y are_congruent_mod m )
assume A6: ( x in a ** X & y in a ** X & x <> y ) ; :: thesis: not x,y are_congruent_mod m
then consider z1 being Integer such that
A7: ( z1 in X & x = a * z1 ) by Th3;
consider z2 being Integer such that
A8: ( z2 in X & y = a * z2 ) by A6, Th3;
not z1,z2 are_congruent_mod m by A7, A6, A8, A1, Th24;
hence not x,y are_congruent_mod m by A7, A8, A1, INT_4:9; :: thesis: verum

end;

for x being Integer st x in a ** X holds
x,m are_coprime

proof

let x be Integer; :: thesis: ( x in a ** X implies x,m are_coprime )
assume x in a ** X ; :: thesis: x,m are_coprime
then consider y being Integer such that
A9: ( y in X & x = a * y ) by Th3;
y,m are_coprime by A9, A1, Th24;
hence x,m are_coprime by A9, A1, INT_2:26; :: thesis: verum

end;

hence a ** X is_RRS_of m by A1, A3, A4, A5, Th26; :: thesis: verum