let l be empty quasi-loci; :: thesis: {} is type-distribution of l
reconsider d = {} as PartFunc of Vars,QuasiTypes by RELSET_1:12;
( dom d = rng l & d is even ) ;
hence {} is type-distribution of l by Def30; :: thesis: verum