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;
set q = p | n;
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))%>
A2: dom (p | n) = n

proof

A3: dom (p | n) = (len p) /\ n by RELAT_1:90;
n < len p by A1, XREAL_1:31;
then n c= len p by NAT_1:40;
hence dom (p | n) = n by A3, XBOOLE_1:28; :: thesis: verum

end;

thus (p | n) ^ <%(p . ((len p) - 1))%> = p :: thesis: verum

proof

A4: dom ((p | n) ^ <%(p . ((len p) - 1))%>) = len ((p | n) ^ <%(p . ((len p) - 1))%>)
.= (len (p | n)) + (len <%(p . ((len p) - 1))%>) by AFINSQ_1:20
.= dom p by A1, A2, AFINSQ_1:38 ;
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 A5: x in dom p ; :: thesis: p . x = ((p | n) ^ <%(p . ((len p) - 1))%>) . x
then reconsider k = x as Element of NAT ;
A6: k in n \/ {n} by A1, A5, AFINSQ_1:4;

A7: now

assume A8: k in n ; :: thesis: p . k = ((p | n) ^ <%(p . ((len p) - 1))%>) . k
hence p . k = (p | n) . k by A2, FUNCT_1:70
.= ((p | n) ^ <%(p . ((len p) - 1))%>) . k by A2, A8, AFINSQ_1:def 4 ;
:: thesis: verum

end;

now

assume A9: k in {n} ; :: thesis: ((p | n) ^ <%(p . ((len p) - 1))%>) . k = p . k
A10: 0 in dom <%(p . ((len p) - 1))%> by NAT_1:45;
thus ((p | n) ^ <%(p . ((len p) - 1))%>) . k = ((p | n) ^ <%(p . ((len p) - 1))%>) . ((len (p | n)) + 0 ) by A2, A9, TARSKI:def 1
.= <%(p . ((len p) - 1))%> . 0 by A10, AFINSQ_1:def 4
.= p . n by A1, AFINSQ_1:def 5
.= p . k by A9, TARSKI:def 1 ; :: thesis: verum

end;

hence p . x = ((p | n) ^ <%(p . ((len p) - 1))%>) . x by A6, A7, XBOOLE_0:def 3; :: thesis: verum

end;

hence (p | n) ^ <%(p . ((len p) - 1))%> = p by A4, FUNCT_1:9; :: thesis: verum

end;