theorem Th54: :: FLANG_1:54

for E being set
for A being Subset of (E ^omega) st <%> E in A holds
( A * = (A *) ^^ A & A * = A ^^ (A *) )