let x, E be set ; :: thesis: for A being Subset of (E ^omega )
for k being Nat st A |^.. k = {x} holds
x = <%> E
let A be Subset of (E ^omega ); :: thesis: for k being Nat st A |^.. k = {x} holds
x = <%> E
let k be Nat; :: thesis: ( A |^.. k = {x} implies x = <%> E )
assume A1: ( A |^.. k = {x} & x <> <%> E ) ; :: thesis: contradiction
then A2: x in A |^.. k by ZFMISC_1:37;
A3: A |^.. (k + k) c= A |^.. k by Th5, NAT_1:11;
reconsider a = x as Element of E ^omega by A1, ZFMISC_1:37;
A4: a ^ a in A |^.. (k + k) by A2, Th37;
a ^ a <> x by A1, FLANG_1:12;
hence contradiction by A1, A3, A4, TARSKI:def 1; :: thesis: verum