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

proof

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

A6: now :: thesis: ( k in n implies p . k = ((p | n) ^ <%(p . ((len p) - 1))%>) . k )

assume A7: k in n ; :: thesis: p . k = ((p | n) ^ <%(p . ((len p) - 1))%>) . k
hence p . k = (p | n) . k by A3, FUNCT_1:47
.= ((p | n) ^ <%(p . ((len p) - 1))%>) . k by A3, A7, Def3 ;
:: thesis: verum

end;

A8: now :: thesis: ( k in {n} implies ((p | n) ^ <%(p . ((len p) - 1))%>) . k = p . k )

0 in Segm (0 + 1) by NAT_1:45;
then A9: 0 in dom <%(p . ((len p) - 1))%> by Def4;
assume A10: k in {n} ; :: thesis: ((p | n) ^ <%(p . ((len p) - 1))%>) . k = p . k
hence ((p | n) ^ <%(p . ((len p) - 1))%>) . k = ((p | n) ^ <%(p . ((len p) - 1))%>) . ((len (p | n)) + 0) by A3, TARSKI:def 1
.= <%(p . ((len p) - 1))%> . 0 by A9, Def3
.= p . k by A1, A10, TARSKI:def 1 ;
:: thesis: verum

end;

k in (Segm n) \/ {n} by A5, Th1, A2;
hence p . x = ((p | n) ^ <%(p . ((len p) - 1))%>) . x by A6, A8, XBOOLE_0:def 3; :: thesis: verum

end;

take p | n ; :: thesis: ex x being object st p = (p | n) ^ <%x%>
take p . ((len p) - 1) ; :: thesis: p = (p | n) ^ <%(p . ((len p) - 1))%>
dom ((p | n) ^ <%(p . ((len p) - 1))%>) = (len (p | n)) + (len <%(p . ((len p) - 1))%>) by Def3
.= dom p by A1, A3, Th30 ;
hence (p | n) ^ <%(p . ((len p) - 1))%> = p by A4; :: thesis: verum