let E be non empty set ; :: thesis: for u being Element of E ^omega st len u = 1 holds

ex e being Element of E st

( <%e%> = u & e = u . 0 )

let u be Element of E ^omega ; :: thesis: ( len u = 1 implies ex e being Element of E st

( <%e%> = u & e = u . 0 ) )

assume len u = 1 ; :: thesis: ex e being Element of E st

( <%e%> = u & e = u . 0 )

then len u = 0 + 1 ;

then consider v being Element of E ^omega , e being Element of E such that

A1: len v = 0 and

A2: u = v ^ <%e%> by FLANG_1:7;

take e ; :: thesis: ( <%e%> = u & e = u . 0 )

v = <%> E by A1;

then u = {} ^ <%e%> by A2;

then u = <%e%> ;

hence ( <%e%> = u & e = u . 0 ) ; :: thesis: verum

ex e being Element of E st

( <%e%> = u & e = u . 0 )

let u be Element of E ^omega ; :: thesis: ( len u = 1 implies ex e being Element of E st

( <%e%> = u & e = u . 0 ) )

assume len u = 1 ; :: thesis: ex e being Element of E st

( <%e%> = u & e = u . 0 )

then len u = 0 + 1 ;

then consider v being Element of E ^omega , e being Element of E such that

A1: len v = 0 and

A2: u = v ^ <%e%> by FLANG_1:7;

take e ; :: thesis: ( <%e%> = u & e = u . 0 )

v = <%> E by A1;

then u = {} ^ <%e%> by A2;

then u = <%e%> ;

hence ( <%e%> = u & e = u . 0 ) ; :: thesis: verum