let C1, C2 be Subset of A; ( 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 H1( 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) = H1(n,F1 . n)
; ( 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) = H1(n,F2 . n)
; 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) = H1(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) = H1(n,F2 . n)
by A12;
F1 = F2
from NAT_1:sch 15(A13, A14, A15, A16, A17, A18);
hence
C1 = C2
by A7, A10; verum