:: deftheorem Def2 defines |^ FLANG_1:def 2 :
for E being set
for A being Subset of (E ^omega)
for n being Nat
for b₄ being Subset of (E ^omega) holds
( b₄ = A |^ n iff ex concat being sequence of (bool (E ^omega)) st
( b₄ = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) );