theorem :: FLANG_1:53

for E being set
for A being Subset of (E ^omega) holds
( (A *) ^^ A c= A * & A ^^ (A *) c= A * ) by Th52;