:: deftheorem Def3 defines QuasiLoci ABCMIZ_1:def 3 :
for b₁ being FinSequenceSet of Vars holds
( b₁ = QuasiLoci iff for p being FinSequence of Vars holds
( p in b₁ iff ( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p dom i) ) ) ) );