theorem Th37: :: FLANG_2:37

for E being set
for A being Subset of (E ^omega)
for k, l, m, n being Nat st m <= n & k <= l holds
(A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))