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:8;
then len p <= len q by FINSEQ_1:7;
then reconsider N = (len q) - (len p) as Element of NAT by INT_1:16, XREAL_1:50;
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:35
.= len q ;

now

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₁
A8: k in NAT by ORDINAL1:def 13;
then k in Seg (len q) by A5, A6, A7;
then A9: 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, A8;
then A10: k in dom p by FINSEQ_1:def 3;
hence (p ^ f) . k = p . k by FINSEQ_1:def 7
.= q . k by A1, A10, GRFUNC_1:8 ;
:: thesis: verum

end;

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

then k - (len p) > 0 by XREAL_1:52;
then reconsider kk = k - (len p) as Element of NAT by INT_1:16;
k <= (len p) + (len f) by A7, FINSEQ_1:35;
then A12: kk <= ((len p) + (len f)) - (len p) by XREAL_1:11;
k - (len p) >= 0 + 1 by A11, INT_1:20, XREAL_1:52;
then A13: kk in Seg (len f) by A12;
then A14: kk in dom f by FINSEQ_1:def 3;
thus (p ^ f) . k = f . kk by A7, A11, FINSEQ_1:37
.= f /. kk by A14, PARTFUN1:def 8
.= q /. ((len p) + kk) by A3, A4, A13
.= q . k by A9, PARTFUN1:def 8 ; :: thesis: verum

end;

end;

end;

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