let D be non empty set ; :: thesis: for p, q being FinSequence of D st p c= q holds
ex p9 being FinSequence of D st p ^ p9 = q
let p, q be FinSequence of D; :: thesis: ( p c= q implies ex p9 being FinSequence of D st p ^ p9 = q )
assume A1: p c= q ; :: thesis: ex p9 being FinSequence of D st p ^ p9 = q
( dom p = Seg (len p) & dom q = Seg (len q) ) by FINSEQ_1:def 3;
then Seg (len p) c= Seg (len q) by A1, GRFUNC_1:2;
then len p <= len q by FINSEQ_1:5;
then reconsider N = (len q) - (len p) as Element of NAT by INT_1:3, XREAL_1:48;
defpred S₁[ Nat, set ] means q /. ((len p) + $1) = $2;
A2: for n being Nat st n in Seg N holds
ex d being Element of D st S₁[n,d] ;
consider f being FinSequence of D such that
A3: len f = N and
A4: for n being Nat st n in Seg N holds
S₁[n,f /. n] from FINSEQ_4:sch 1(A2);
take f ; :: thesis: p ^ f = q
A5: len (p ^ f) = (len p) + N by A3, FINSEQ_1:22
.= len q ;

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

let k be Nat; :: thesis: ( 1 <= k & k <= len (p ^ f) implies (p ^ f) . b₁ = q . b₁ )
assume that
A6: 1 <= k and
A7: k <= len (p ^ f) ; :: thesis: (p ^ f) . b₁ = q . b₁
k in Seg (len q) by A5, A6, A7;
then A8: k in dom q by FINSEQ_1:def 3;

per cases ( k <= len p or len p < k ) ;

suppose k <= len p ; :: thesis: (p ^ f) . b₁ = q . b₁

then k in Seg (len p) by A6;
then A9: k in dom p by FINSEQ_1:def 3;
hence (p ^ f) . k = p . k by FINSEQ_1:def 7
.= q . k by A1, A9, GRFUNC_1:2 ;
:: thesis: verum

end;

suppose A10: len p < k ; :: thesis: (p ^ f) . b₁ = q . b₁

then k - (len p) > 0 by XREAL_1:50;
then reconsider kk = k - (len p) as Element of NAT by INT_1:3;
k <= (len p) + (len f) by A7, FINSEQ_1:22;
then A11: kk <= ((len p) + (len f)) - (len p) by XREAL_1:9;
k - (len p) >= 0 + 1 by A10, INT_1:7, XREAL_1:50;
then A12: kk in Seg (len f) by A11;
then A13: kk in dom f by FINSEQ_1:def 3;
thus (p ^ f) . k = f . kk by A7, A10, FINSEQ_1:24
.= f /. kk by A13, PARTFUN1:def 6
.= q /. ((len p) + kk) by A3, A4, A12
.= q . k by A8, PARTFUN1:def 6 ; :: thesis: verum

end;

end;

end;

hence p ^ f = q by A5; :: thesis: verum