let E be set ; :: thesis: (Lex E) * = E ^omega

A1: now :: thesis: for x being object st x in E ^omega holds
x in (Lex E) *

let x be object ; :: thesis: ( x in E ^omega implies x in (Lex E) * )
assume x in E ^omega ; :: thesis: x in (Lex E) *
then reconsider a = x as Element of E ^omega ;
a in (Lex E) |^ (len a) by Th73;
hence x in (Lex E) * by Th41; :: thesis: verum

end;

for x being object st x in (Lex E) * holds
x in E ^omega ;
hence (Lex E) * = E ^omega by A1, TARSKI:2; :: thesis: verum