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 Th79, 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, Th22;

now :: thesis: for k being Nat st 1 <= k & k <= len p holds
p . k = (r ^ q) . k

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: now :: thesis: ( k <= len r implies p . k = (r ^ q) . k )

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

end;

now :: thesis: ( not k <= len r implies p . k = (r ^ q) . k )

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

end;

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

end;

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