theorem Th10: :: FLANG_2:10

for E, x being set
for A being Subset of (E ^omega)
for m, n being Nat st m <> n & A |^ m = {x} & A |^ n = {x} holds
x = <%> E