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