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 such that
A4: Vars = Union V and
A1: V . 0 = { [{} ,k] where k is Element of NAT : verum } and
A2: 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 VARSdef;
consider j being Element of NAT such that
A3: A c= V . j by A1, A2, Lem2;
( V . (j + 1) = { [(varcl B),k] where B is Subset of (V . j), k is Element of NAT : B is finite } & i in NAT ) by A2, ORDINAL1:def 13;
then ( [(varcl A),i] in V . (j + 1) & dom V = NAT ) by A3, PARTFUN1:def 4;
hence [(varcl A),i] in Vars by A4, CARD_5:10; :: thesis: verum