let D be non empty set ; :: thesis: for p, q being FinSequence of D st p c= q holds
ex p' being FinSequence of D st p ^ p' = q
let p, q be FinSequence of D; :: thesis: ( p c= q implies ex p' being FinSequence of D st p ^ p' = q )
assume A1: p c= q ; :: thesis: ex p' being FinSequence of D st p ^ p' = q
defpred S₁[ Nat, set ] means q /. ((len p) + $1) = $2;
A2: dom p = Seg (len p) by FINSEQ_1:def 3;
dom q = Seg (len q) by FINSEQ_1:def 3;
then Seg (len p) c= Seg (len q) by A1, A2, 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;
A3: 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
A4: len f = N and
A5: for n being Nat st n in Seg N holds
S₁[n,f /. n] from FINSEQ_4:sch 1(A3);
take f ; :: thesis: p ^ f = q
A6: len (p ^ f) = (len p) + N by A4, FINSEQ_1:35
.= len q ;

now

let k be Nat; :: thesis: ( 1 <= k & k <= len (p ^ f) implies (p ^ f) . b₁ = q . b₁ )
assume A7: ( 1 <= k & 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 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 A7, 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 A12: k - (len p) > 0 by XREAL_1:52;
A13: k - (len p) >= 0 + 1 by A11, INT_1:20, XREAL_1:52;
reconsider kk = k - (len p) as Element of NAT by A12, INT_1:16;
k <= (len p) + (len f) by A7, FINSEQ_1:35;
then kk <= ((len p) + (len f)) - (len p) by XREAL_1:11;
then A14: kk in Seg (len f) by A13;
then A15: kk in dom f by FINSEQ_1:def 3;
thus (p ^ f) . k = f . kk by A7, A11, FINSEQ_1:37
.= f /. kk by A15, PARTFUN1:def 8
.= q /. ((len p) + kk) by A4, A5, A14
.= q . k by A9, PARTFUN1:def 8 ; :: thesis: verum

end;

end;

end;

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