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

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