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 consider e being Element of E such that
A: ( e in E & u = <%e%> ) by FLANG_1:def 4;
thus len u = 1 by A, AFINSQ_1:def 5; :: thesis: verum

end;

assume len u = 1 ; :: thesis: u in Lex E
then consider e being Element of E such that
B: ( <%e%> = u & e = u . 0 ) by LmXSeq10;
thus u in Lex E by B, FLANG_1:def 4; :: thesis: verum