let E, x 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 that
A1: A |^.. k = {x} and
A2: x <> <%> E ; :: thesis: contradiction
reconsider a = x as Element of E ^omega by A1, ZFMISC_1:31;
x in A |^.. k by A1, ZFMISC_1:31;
then A3: a ^ a in A |^.. (k + k) by Th37;
A4: A |^.. (k + k) c= A |^.. k by Th5, NAT_1:11;
a ^ a <> x by A2, FLANG_1:11;
hence contradiction by A1, A4, A3, TARSKI:def 1; :: thesis: verum