let A1, A2 be set ; :: thesis: ( ex V being ManySortedSet of NAT st
( A1 = 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 } ) ) & ex V being ManySortedSet of NAT st
( A2 = 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 } ) ) implies A1 = A2 )
given V1 being ManySortedSet of NAT such that A4: A1 = Union V1 and
A5: V1 . 0 = { [{},i] where i is Element of NAT : verum } and
A6: for n being Nat holds V1 . (n + 1) = H₁(n,V1 . n) ; :: thesis: ( for V being ManySortedSet of NAT holds
( not A2 = Union V or not V . 0 = { [{},i] where i is Element of NAT : verum } or ex n being Nat st not V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) or A1 = A2 )
given V2 being ManySortedSet of NAT such that A7: A2 = Union V2 and
A8: V2 . 0 = { [{},i] where i is Element of NAT : verum } and
A9: for n being Nat holds V2 . (n + 1) = H₁(n,V2 . n) ; :: thesis: A1 = A2
A10: dom V1 = NAT by PARTFUN1:def 2;
A11: dom V2 = NAT by PARTFUN1:def 2;
V1 = V2 from NAT_1:sch 15(A10, A5, A6, A11, A8, A9);
hence A1 = A2 by A4, A7; :: thesis: verum