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
B: ( len v = 0 & u = v ^ <%e%> ) by FLANG_1:7;
take e ; :: thesis: ( <%e%> = u & e = u . 0 )
v = <%> E by B;
then u = <%e%> by B, AFINSQ_1:32;
hence ( <%e%> = u & e = u . 0 ) by AFINSQ_1:38; :: thesis: verum