theorem Th57: :: FLANG_1:57

for E being set
for A being Subset of (E ^omega) holds A ^^ (A *) = (A *) ^^ A