:: deftheorem Def4 defines |^ FVALUAT1:def 4 :
for K being non empty doubleLoopStr
for S being Subset of K
for n being Nat
for b₄ being Subset of K holds
( ( n = 0 implies ( b₄ = S |^ n iff b₄ = the carrier of K ) ) & ( not n = 0 implies ( b₄ = S |^ n iff ex f being FinSequence of bool the carrier of K st
( b₄ = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = S *' (f /. i) ) ) ) ) );