consider V being ManySortedSet of NAT such that
A1: Vars = Union V and
A2: V . 0 = { [{},i] where i is Element of NAT : verum } and
for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } by Def2;
dom V = NAT by PARTFUN1:def 2;
then V . 0 in rng V by FUNCT_1:def 3;
hence { [{},i] where i is Element of NAT : verum } c= Vars by A1, A2, ZFMISC_1:74; :: thesis: verum