theorem Th7: :: FLANG_1:7

for E being set
for b being Element of E ^omega
for n being Nat st len b = n + 1 holds
ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = c ^ <%e%> )