:: deftheorem defines |^ FLANG_2:def 1 :
for E being set
for A being Subset of (E ^omega)
for m, n being Nat holds A |^ (m,n) = union { B where B is Subset of (E ^omega) : ex k being Nat st
( m <= k & k <= n & B = A |^ k ) } ;