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