let p be FinSequence; :: thesis: ( p <> {} implies ex q being FinSequence ex x being set st p = q ^ <*x*> )
assume p <> {} ; :: thesis: ex q being FinSequence 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;
reconsider q = p | (Seg n) as FinSequence by Th19;
take q ; :: thesis: ex x being set st p = q ^ <*x*>
take p . (len p) ; :: thesis: p = q ^ <*(p . (len p))*>
A2: dom q = (dom p) /\ (Seg n) by RELAT_1:61
.= (Seg (len p)) /\ (Seg n) by Def3 ;
n <= len p by A1, NAT_1:11;
then Seg n c= Seg (len p) by Th7;
then A3: dom q = Seg n by A2, XBOOLE_1:28;
A4: dom (q ^ <*(p . (len p))*>) = Seg (len (q ^ <*(p . (len p))*>)) by Def3
.= Seg ((len q) + (len <*(p . (len p))*>)) by Th35
.= Seg ((len q) + 1) by Th56
.= Seg (len p) by A1, A3, Def3
.= dom p by Def3 ;
for x being set st x in dom p holds
p . x = (q ^ <*(p . (len p))*>) . x

proof

let x be set ; :: thesis: ( x in dom p implies p . x = (q ^ <*(p . (len p))*>) . x )
assume A5: x in dom p ; :: thesis: p . x = (q ^ <*(p . (len p))*>) . x
then reconsider k = x as Element of NAT ;
k in Seg (n + 1) by A1, A5, Def3;
then A6: k in (Seg n) \/ {(n + 1)} by Th11;

A7: now

assume A8: k in Seg n ; :: thesis: p . k = (q ^ <*(p . (len p))*>) . k
hence p . k = q . k by A3, FUNCT_1:47
.= (q ^ <*(p . (len p))*>) . k by A3, A8, Def7 ;
:: thesis: verum

end;

now

assume A9: k in {(n + 1)} ; :: thesis: (q ^ <*(p . (len p))*>) . k = p . k
1 in Seg 1 ;
then A10: 1 in dom <*(p . (len p))*> by Def8;
thus (q ^ <*(p . (len p))*>) . k = (q ^ <*(p . (len p))*>) . (n + 1) by A9, TARSKI:def 1
.= (q ^ <*(p . (len p))*>) . ((len q) + 1) by A3, Def3
.= <*(p . (len p))*> . 1 by A10, Def7
.= p . (n + 1) by A1, Def8
.= p . k by A9, TARSKI:def 1 ; :: thesis: verum

end;

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

end;

hence q ^ <*(p . (len p))*> = p by A4, FUNCT_1:2; :: thesis: verum