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
reconsider a = x as Element of E ^omega by A1, ZFMISC_1:31;
x in A * by A1, ZFMISC_1:31;
then A3: a ^ a in A * by Th45;
a ^ a <> x by A2, Th11;
hence contradiction by A1, A3, TARSKI:def 1; :: thesis: verum