theorem :: FLANG_3:42

for E being set
for A being Subset of (E ^omega)
for k being Nat holds (A |^.. k) ^^ (A ?) = (A ?) ^^ (A |^.. k)