let l be empty quasi-loci; :: thesis: {} is type-distribution of l
reconsider d = {} as PartFunc of Vars,QuasiTypes by RELSET_1:12;
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 Def29;
hence {} is type-distribution of l by Def30; :: thesis: verum