let V be ManySortedSet of NAT ; ( V . 0 = { [{},i] where i is Element of NAT : verum } & ( 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 } ) implies for A being finite Subset of Vars ex i being Element of NAT st A c= V . i )
assume that
A1:
V . 0 = { [{},i] where i is Element of NAT : verum }
and
A2:
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 }
; for A being finite Subset of Vars ex i being Element of NAT st A c= V . i
let A be finite Subset of Vars; ex i being Element of NAT st A c= V . i
A3:
Vars = Union V
by A1, A2, Def2;
defpred S1[ object , object ] means $1 in V . $2;
consider f being Function such that
A9:
( dom f = A & rng f c= NAT )
and
A10:
for x being object st x in A holds
S1[x,f . x]
from FUNCT_1:sch 6(A4);