:: deftheorem Def8 defines |^ AOFA_000:def 8 :
for A being non-empty UAStr
for B being Subset of A
for n being natural Number
for b₄ being Subset of A holds
( b₄ = B |^ n iff ex F being sequence of (bool the carrier of A) st
( b₄ = 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 ) } ) ) );