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 4;
then V . 0 in rng V by FUNCT_1:def 5;
hence { [{} ,i] where i is Element of NAT : verum } c= Vars by A1, A2, ZFMISC_1:92; :: thesis: verum