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 12;
set q = p | n;
n <= len p by A1, NAT_1:11;
then ( dom (p | n) = (len p) /\ n & n c= len p ) by NAT_1:39, RELAT_1:61;
then A2: dom (p | n) = n by XBOOLE_1:28;
A3: for x being set st x in dom p holds
p . x = ((p | n) ^ <%(p . ((len p) - 1))%>) . x

proof

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

A5: now

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

end;

A7: now

0 in 0 + 1 by NAT_1:45;
then A8: 0 in dom <%(p . ((len p) - 1))%> by Def5;
assume A9: 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 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 = ((p | n) ^ <%(p . ((len p) - 1))%>) . x by A5, A7, XBOOLE_0:def 3; :: thesis: verum

end;

take p | n ; :: thesis: ex x being set 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 Def4
.= dom p by A1, A2, Th36 ;
hence (p | n) ^ <%(p . ((len p) - 1))%> = p by A3, FUNCT_1:2; :: thesis: verum