consider f being Function such that
A1: dom f = NAT and
A2: f . 0 = { [{},i] where i is Element of NAT : verum } and
A3: for n being Nat holds f . (n + 1) = H₁(n,f . n) from NAT_1:sch 11();
reconsider f = f as ManySortedSet of NAT by A1, PARTFUN1:def 2, RELAT_1:def 18;
take Union f ; :: thesis: ex V being ManySortedSet of NAT st
( Union f = Union V & 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 } ) )
take V = f; :: thesis: ( Union f = Union V & 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 } ) )
thus Union f = Union V ; :: thesis: ( 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 } ) )
thus V . 0 = { [{},i] where i is Element of NAT : verum } by A2; :: thesis: 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 }
let n be Nat; :: thesis: V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite }
thus V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } by A3; :: thesis: verum