theorem Th38: :: FLANG_3:38

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