theorem Th45: :: FLANG_3:45

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