theorem Th72: :: FLANG_2:72

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