theorem Th5: :: FSM_3:5

for E being non empty set
for u being Element of E ^omega
for k being Nat st k <> 0 & len u <= k + 1 holds
ex v1, v2 being Element of E ^omega st
( len v1 <= k & len v2 <= k & u = v1 ^ v2 )