for m being Element of NAT
for a being Integer
for X being finite Subset of INT st a,m are_coprime & X is_CRS_of m holds
a ** X is_CRS_of m