theorem Th73: :: FLANG_1:73

for E being set
for a being Element of E ^omega holds a in (Lex E) |^ (len a)