let E be non empty set ; :: thesis: for u being Element of E ^omega st len u > 0 holds
ex e being Element of E ex u1 being Element of E ^omega st u = <%e%> ^ u1
let u be Element of E ^omega ; :: thesis: ( len u > 0 implies ex e being Element of E ex u1 being Element of E ^omega st u = <%e%> ^ u1 )
assume len u > 0 ; :: thesis: ex e being Element of E ex u1 being Element of E ^omega st u = <%e%> ^ u1
then consider k being Nat such that
A1: len u = k + 1 by NAT_1:6;
ex u1 being Element of E ^omega ex e being Element of E st
( len u1 = k & u = <%e%> ^ u1 ) by A1, FLANG_1:9;
hence ex e being Element of E ex u1 being Element of E ^omega st u = <%e%> ^ u1 ; :: thesis: verum