theorem :: FLANG_1:51

for E being set
for A being Subset of (E ^omega)
for m being Nat holds
( A |^ (m + 1) c= (A *) ^^ A & A |^ (m + 1) c= A ^^ (A *) ) by Th50;