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
A3: 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;
defpred S₁[ Nat] means varcl (V . $1) = V . $1;

end;

let i be Nat; :: thesis:
assume A7: S₁[i] ; :: thesis:
reconsider i9 = i as Element of NAT by ORDINAL1:def 12;
A8: V . (i + 1) = { [(varcl A),j] where A is Subset of (V . i), j is Element of NAT : A is finite } by A3;

let x, y be set ; :: thesis:
assume [x,y] in V . (i + 1) ; :: thesis:
then consider A being Subset of (V . i), j being Element of NAT such that
A9: [x,y] = [(varcl A),j] and
A is finite by A8;
x = varcl A by A9, XTUPLE_0:1;
then A10: x c= V . i by A7, Th9;
V . i9 c= V . (i9 + 1) by A2, A3, Th14, NAT_1:11;
hence x c= V . (i + 1) by A10; :: thesis:

end;

end;

A12: for i being Nat holds S₁[i] from NAT_1:sch 2(A5, A6);
A13: varcl Vars = union { (varcl a) where a is Element of rng V : verum } by A1, Th10;

let x be object ; :: thesis:
assume x in varcl Vars ; :: thesis:
then consider Y being set such that
A14: x in Y and
A15: Y in { (varcl a) where a is Element of rng V : verum } by A13, TARSKI:def 4;
consider a being Element of rng V such that
A16: Y = varcl a by A15;
consider i being object such that
A17: i in dom V and
A18: a = V . i by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A17;
varcl (V . i) = a by A12, A18;
hence x in Vars by A1, A14, A16, A17, A18, CARD_5:2; :: thesis:

end;