theorem :: FLANG_1:69

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