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;
take q ; :: thesis: ex x being set st p = q ^ <%x%>
take p . ((len p) - 1) ; :: thesis: p = q ^ <%(p . ((len p) - 1))%>
A2: dom q = n

proof

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

end;

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

proof

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

A7: now

assume A8: 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, A8, Def4 ;
:: thesis: verum

end;

now

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

end;

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

end;

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

end;