let x, E 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 )
assume ( A + = {x} & x <> <%> E ) ; :: thesis: contradiction
then ( A |^.. 1 = {x} & x <> <%> E ) by Th50;
hence contradiction by Th38; :: thesis: verum