consider V being ManySortedSet of such that
A1: Vars = Union V and
A2: V . 0 = { [{} ,i] where i is Element of NAT : verum } and
A0: 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 VARSdef;
set X = { [(varcl A),j] where A is Subset of Vars , j is Element of NAT : A is finite } ;
B1: dom V = NAT by PARTFUN1:def 4;
defpred S₁[ Nat] means V . $1 c= { [(varcl A),j] where A is Subset of Vars , j is Element of NAT : A is finite } ;
A3: S₁[ 0 ]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in V . 0 or x in { [(varcl A),j] where A is Subset of Vars , j is Element of NAT : A is finite } )
assume x in V . 0 ; :: thesis: x in { [(varcl A),j] where A is Subset of Vars , j is Element of NAT : A is finite }
then ( {} c= Vars & ex i being Element of NAT st x = [{} ,i] ) by A2, XBOOLE_1:2;
hence x in { [(varcl A),j] where A is Subset of Vars , j is Element of NAT : A is finite } by Th11; :: thesis: verum

end;

A4: now

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume S₁[i] ; :: thesis: S₁[i + 1]
A6: V . (i + 1) = { [(varcl A),j] where A is Subset of (V . i), j is Element of NAT : A is finite } by A0;
thus S₁[i + 1] :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in V . (i + 1) or x in { [(varcl A),j] where A is Subset of Vars , j is Element of NAT : A is finite } )
assume x in V . (i + 1) ; :: thesis: x in { [(varcl A),j] where A is Subset of Vars , j is Element of NAT : A is finite }
then consider A being Subset of (V . i), j being Element of NAT such that
A7: ( x = [(varcl A),j] & A is finite ) by A6;
V . i in rng V by B1, FUNCT_1:def 5;
then V . i c= Vars by A1, ZFMISC_1:92;
then A c= Vars by XBOOLE_1:1;
hence x in { [(varcl A),j] where A is Subset of Vars , j is Element of NAT : A is finite } by A7; :: thesis: verum

end;

end;

A8: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A3, A4);

now

let x be set ; :: thesis: ( x in rng V implies x c= { [(varcl A),j] where A is Subset of Vars , j is Element of NAT : A is finite } )
assume x in rng V ; :: thesis: x c= { [(varcl A),j] where A is Subset of Vars , j is Element of NAT : A is finite }
then ex y being set st
( y in NAT & x = V . y ) by B1, FUNCT_1:def 5;
hence x c= { [(varcl A),j] where A is Subset of Vars , j is Element of NAT : A is finite } by A8; :: thesis: verum

end;

hence Vars c= { [(varcl A),j] where A is Subset of Vars , j is Element of NAT : A is finite } by A1, ZFMISC_1:94; :: according to XBOOLE_0:def 10 :: thesis: { [(varcl A),j] where A is Subset of Vars , j is Element of NAT : A is finite } c= Vars
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { [(varcl A),j] where A is Subset of Vars , j is Element of NAT : A is finite } or x in Vars )
assume x in { [(varcl A),j] where A is Subset of Vars , j is Element of NAT : A is finite } ; :: thesis: x in Vars
then ex A being Subset of Vars ex j being Element of NAT st
( x = [(varcl A),j] & A is finite ) ;
hence x in Vars by Lem3; :: thesis: verum