theorem Th4: :: FSM_3:4

for E being non empty set
for u being Element of E ^omega st len u = 1 holds
ex e being Element of E st
( <%e%> = u & e = u . 0 )