theorem Th7: :: FSM_3:7

for E being non empty set
for u being Element of E ^omega st len u > 0 holds
ex e being Element of E ex u1 being Element of E ^omega st u = <%e%> ^ u1