for i being Nat st i in dom {} holds
((<*> Vars) . i) `1 c= rng ((<*> Vars) | i) ;
hence <*> Vars in QuasiLoci by Def3; :: thesis: verum