theorem Th35: :: FLANG_2:35
for E being set
for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ (m,n)) ^^ (A |^ k) = (A |^ k) ^^ (A |^ (m,n))