let C1, C2 be Subset of A; :: thesis: ( ex F being sequence of (bool the carrier of A) st
( C1 = F . n & F . 0 = B & ( for n being Nat holds F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) } ) ) & ex F being sequence of (bool the carrier of A) st
( C2 = F . n & F . 0 = B & ( for n being Nat holds F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) } ) ) implies C1 = C2 )
deffunc H₁( set , set ) -> set = $2 \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= $2 ) } ;
given F1 being sequence of (bool the carrier of A) such that A7: C1 = F1 . n and
A8: F1 . 0 = B and
A9: for n being Nat holds F1 . (n + 1) = H₁(n,F1 . n) ; :: thesis: ( for F being sequence of (bool the carrier of A) holds
( not C2 = F . n or not F . 0 = B or ex n being Nat st not F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) } ) or C1 = C2 )
given F2 being sequence of (bool the carrier of A) such that A10: C2 = F2 . n and
A11: F2 . 0 = B and
A12: for n being Nat holds F2 . (n + 1) = H₁(n,F2 . n) ; :: thesis: C1 = C2
A13: dom F1 = NAT by FUNCT_2:def 1;
A14: F1 . 0 = B by A8;
A15: for n being Nat holds F1 . (n + 1) = H₁(n,F1 . n) by A9;
A16: dom F2 = NAT by FUNCT_2:def 1;
A17: F2 . 0 = B by A11;
A18: for n being Nat holds F2 . (n + 1) = H₁(n,F2 . n) by A12;
F1 = F2 from NAT_1:sch 15(A13, A14, A15, A16, A17, A18);
hence C1 = C2 by A7, A10; :: thesis: verum