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 by Th76
.= {(<%> E)} \/ (A \ {(<%> E)}) by XBOOLE_1:39
.= (A \ {(<%> E)}) ? by Th76 ; :: thesis: verum