theorem Th22: :: FLANG_2:22

for E being set
for A being Subset of (E ^omega)
for m being Nat holds A |^ (m,m) = A |^ m