:: deftheorem defines is_RRS_of INT_8:def 2 :
for X being set
for m being Nat holds
( X is_RRS_of m iff ex fp being FinSequence of INT st
( len fp = len (Sgm (RelPrimes m)) & ( for d being Element of NAT st d in dom fp holds
fp . d in Class ((Cong m),((Sgm (RelPrimes m)) . d)) ) & X = rng fp ) );