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 )

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

( 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
len u = 1
; :: thesis: u in Lex E
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;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

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