theorem Th53: :: FLANG_3:53

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