let E be set ; :: thesis: for b being Element of E ^omega
for n being Nat st len b = n + 1 holds
ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = c ^ <%e%> )
let b be Element of E ^omega ; :: thesis: for n being Nat st len b = n + 1 holds
ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = c ^ <%e%> )
let n be Nat; :: thesis: ( len b = n + 1 implies ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = c ^ <%e%> ) )
assume A1: len b = n + 1 ; :: thesis: ex c being Element of E ^omega ex e being Element of E st
( len c = n & b = c ^ <%e%> )
then b <> {} ;
then consider c9 being XFinSequence, x being object such that
A2: b = c9 ^ <%x%> by AFINSQ_1:40;
<%x%> is Element of E ^omega by A2, Th5;
then reconsider e = x as Element of E by Th6;
reconsider c = c9 as Element of E ^omega by A2, Th5;
take c ; :: thesis: ex e being Element of E st
( len c = n & b = c ^ <%e%> )
take e ; :: thesis: ( len c = n & b = c ^ <%e%> )
n + 1 = (len c) + (len <%x%>) by A1, A2, AFINSQ_1:17
.= (len c) + 1 by AFINSQ_1:34 ;
hence ( len c = n & b = c ^ <%e%> ) by A2; :: thesis: verum