reconsider p = <*> Vars as FinSequence of Vars ;
( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p dom i) ) ) ;
hence <*> Vars in QuasiLoci by Def3; :: thesis: verum