let E, x be set ; :: thesis: for A being Subset of (E ^omega) st A ? = {x} holds
x = <%> E
let A be Subset of (E ^omega); :: thesis: ( A ? = {x} implies x = <%> E )
A ? = A |^ (0,1) by Th79;
hence ( A ? = {x} implies x = <%> E ) by Th52; :: thesis: verum