let A be finite Subset of Vars; :: thesis: for i being Nat holds [(varcl A),i] in Vars
let i be Nat; :: thesis: [(varcl A),i] in Vars
consider V being ManySortedSet of NAT such that
A1: Vars = Union V and
A2: V . 0 = { [{},k] where k is Element of NAT : verum } and
A3: for n being Nat holds V . (n + 1) = { [(varcl b),j] where b is Subset of (V . n), j is Element of NAT : b is finite } by Def2;
consider j being Element of NAT such that
A4: A c= V . j by A2, A3, Th15;
A5: V . (j + 1) = { [(varcl B),k] where B is Subset of (V . j), k is Element of NAT : B is finite } by A3;
i in NAT by ORDINAL1:def 12;
then A6: [(varcl A),i] in V . (j + 1) by A4, A5;
dom V = NAT by PARTFUN1:def 2;
hence [(varcl A),i] in Vars by A1, A6, CARD_5:2; :: thesis: verum