let n be Nat; :: thesis: for p, r being FinSequence st r = p | (Seg n) holds
ex q being FinSequence st p = r ^ q
let p, r be FinSequence; :: thesis: ( r = p | (Seg n) implies ex q being FinSequence st p = r ^ q )
assume A1: r = p | (Seg n) ; :: thesis: ex q being FinSequence st p = r ^ q
then consider m being Nat such that
A2: len p = (len r) + m by Th100, NAT_1:10;
deffunc H₁( Nat) -> set = p . ((len r) + $1);
consider q being FinSequence such that
A3: ( len q = m & ( for k being Nat st k in dom q holds
q . k = H₁(k) ) ) from FINSEQ_1:sch 2();
take q ; :: thesis: p = r ^ q
A4: len p = len (r ^ q) by A2, A3, Th35;

now

let k be Nat; :: thesis: ( 1 <= k & k <= len p implies p . k = (r ^ q) . k )
assume that
A5: 1 <= k and
A6: k <= len p ; :: thesis: p . k = (r ^ q) . k
A7: k in NAT by ORDINAL1:def 12;

A8: now

assume k <= len r ; :: thesis: p . k = (r ^ q) . k
then A9: k in Seg (len r) by A5, A7;
A10: dom r = Seg (len r) by Def3;
then (r ^ q) . k = r . k by A9, Def7;
hence p . k = (r ^ q) . k by A1, A9, A10, FUNCT_1:47; :: thesis: verum

end;

now

assume A11: not k <= len r ; :: thesis: p . k = (r ^ q) . k
then consider j being Nat such that
A12: k = (len r) + j by NAT_1:10;
k - (len r) = j by A12;
then A13: (r ^ q) . k = q . j by A4, A6, A11, Th37;
j <> 0 by A11, A12;
then A14: 0 + 1 <= j by NAT_1:13;
j <= len q by A2, A3, A6, A12, XREAL_1:6;
then j in Seg m by A3, A14, Th3;
then j in dom q by A3, Def3;
hence p . k = (r ^ q) . k by A3, A12, A13; :: thesis: verum

end;

hence p . k = (r ^ q) . k by A8; :: thesis: verum

end;

hence p = r ^ q by A4, Th18; :: thesis: verum