let l be empty quasi-loci; :: thesis: {} is type-distribution of l
reconsider d = {} as PartFunc of Vars ,QuasiTypes by RELSET_1:25;
for x being variable
for T being quasi-type st x in dom d & T = d . x holds
vars T = vars x ;
then ( dom d = rng l & d is even ) by EV;
hence {} is type-distribution of l by TD; :: thesis: verum