let p be XFinSequence; :: thesis: ( p <> {} implies ex q being XFinSequence ex x being set st p = q ^ <%x%> )
assume p <> {} ; :: thesis: ex q being XFinSequence ex x being set st p = q ^ <%x%>
then consider n being Nat such that
A1: len p = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
reconsider q = p | n as XFinSequence by Th12;
n <= len p by A1, NAT_1:11;
then ( dom q = (len p) /\ n & n c= len p ) by NAT_1:40, RELAT_1:90;
then A2: dom q = n by XBOOLE_1:28;
A3: for x being set st x in dom p holds
p . x = (q ^ <%(p . ((len p) - 1))%>) . x

proof

let x be set ; :: thesis: ( x in dom p implies p . x = (q ^ <%(p . ((len p) - 1))%>) . x )
assume A4: x in dom p ; :: thesis: p . x = (q ^ <%(p . ((len p) - 1))%>) . x
then reconsider k = x as Element of NAT ;

A5: now

assume A6: k in n ; :: thesis: p . k = (q ^ <%(p . ((len p) - 1))%>) . k
hence p . k = q . k by A2, FUNCT_1:70
.= (q ^ <%(p . ((len p) - 1))%>) . k by A2, A6, Def4 ;
:: thesis: verum

end;

A7: now

0 in 0 + 1 by Th1;
then A8: 0 in dom <%(p . ((len p) - 1))%> by Def5;
assume A9: k in {n} ; :: thesis: (q ^ <%(p . ((len p) - 1))%>) . k = p . k
hence (q ^ <%(p . ((len p) - 1))%>) . k = (q ^ <%(p . ((len p) - 1))%>) . ((len q) + 0 ) by A2, TARSKI:def 1
.= <%(p . ((len p) - 1))%> . 0 by A8, Def4
.= p . n by A1, Def5
.= p . k by A9, TARSKI:def 1 ;
:: thesis: verum

end;

k in n \/ {n} by A1, A4, Th4;
hence p . x = (q ^ <%(p . ((len p) - 1))%>) . x by A5, A7, XBOOLE_0:def 3; :: thesis: verum

end;

take q ; :: thesis: ex x being set st p = q ^ <%x%>
take p . ((len p) - 1) ; :: thesis: p = q ^ <%(p . ((len p) - 1))%>
dom (q ^ <%(p . ((len p) - 1))%>) = (len q) + (len <%(p . ((len p) - 1))%>) by Def4
.= dom p by A1, A2, Th36 ;
hence q ^ <%(p . ((len p) - 1))%> = p by A3, FUNCT_1:9; :: thesis: verum