let E be non empty set ; :: thesis: for u being Element of E ^omega holds
( u in Lex E iff len u = 1 )
let u be Element of E ^omega ; :: thesis: ( u in Lex E iff len u = 1 )
thus ( u in Lex E implies len u = 1 ) :: thesis: ( len u = 1 implies u in Lex E )

proof

assume u in Lex E ; :: thesis: len u = 1
then ex e being Element of E st
( e in E & u = <%e%> ) by FLANG_1:def 4;
hence len u = 1 by AFINSQ_1:def 4; :: thesis: verum

end;

assume len u = 1 ; :: thesis: u in Lex E
then ex e being Element of E st
( <%e%> = u & e = u . 0 ) by Th4;
hence u in Lex E by FLANG_1:def 4; :: thesis: verum