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

A1: now

let x be set ; :: 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 Th74;
hence x in (Lex E) * by Th42; :: thesis: verum

end;

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