for i, n being Nat st n > 1 & i,n are_coprime holds
( i is_primitive_root_of n iff for fn being FinSequence of NAT st len fn = Euler n & ( for d being Nat st d in dom fn holds
fn . d = i |^ d ) holds
rng fn is_RRS_of n )