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 A1: ( A * = {x} & x <> <%> E ) ; :: thesis: contradiction
then A2: x in A * by ZFMISC_1:37;
reconsider a = x as Element of E ^omega by A1, ZFMISC_1:37;
A3: a ^ a in A * by A2, Th46;
a ^ a <> x by A1, Th12;
hence contradiction by A1, A3, TARSKI:def 1; :: thesis: verum