let E be set ; :: thesis: for A being Subset of (E ^omega) holds A * = (A \ {(<%> E)}) *
let A be Subset of (E ^omega); :: thesis: A * = (A \ {(<%> E)}) *
thus (A \ {(<%> E)}) * = ((A \ {(<%> E)}) \/ {(<%> E)}) * by Th48, Th68
.= (A \/ {(<%> E)}) * by XBOOLE_1:39
.= A * by Th48, Th68 ; :: thesis: verum