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 )
assume that
A1: A + = {x} and
A2: x <> <%> E ; :: thesis: contradiction
A |^.. 1 = {x} by A1, Th50;
hence contradiction by A2, Th38; :: thesis: verum