:: deftheorem defines is_CRS_of INT_4:def 2 :
for m being Nat
for X being set holds
( X is_CRS_of m iff ex fp being FinSequence of INT st
( X = rng fp & len fp = m & ( for b being Nat st b in dom fp holds
fp . b in Class ((Cong m),(b -' 1)) ) ) );