theorem Th7: :: FLANG_3:7

for E being set
for A being Subset of (E ^omega)
for m, n being Nat st m <= n + 1 holds
(A |^ (m,n)) \/ (A |^.. (n + 1)) = A |^.. m