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 = <%e%> ^ c )
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 = <%e%> ^ c )
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 = <%e%> ^ c ) )
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 = <%e%> ^ c )
then b <> {} ;
then consider c9 being XFinSequence, x being set such that
A2: b = <%x%> ^ c9 by Th8;
<%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 = <%e%> ^ c )
take e ; :: thesis: ( len c = n & b = <%e%> ^ c )
n + 1 = (len c) + (len <%x%>) by A1, A2, AFINSQ_1:17
.= (len c) + 1 by AFINSQ_1:33 ;
hence ( len c = n & b = <%e%> ^ c ) by A2; :: thesis: verum