theorem :: FLANG_3:43

for E being set
for A, B being Subset of (E ^omega)
for k being Nat st B c= A * holds
( (A |^.. k) ^^ B c= A |^.. k & B ^^ (A |^.. k) c= A |^.. k )