theorem Th56: :: FLANG_1:56

for E being set
for A being Subset of (E ^omega) holds
( A * = {(<%> E)} \/ (A ^^ (A *)) & A * = {(<%> E)} \/ ((A *) ^^ A) )