let p, q, r, s be FinSequence; :: thesis: ( p ^ q = r ^ s & len p <= len r implies ex t, u being FinSequence st
( p ^ t = r & u ^ s = q ) )
assume A1: ( p ^ q = r ^ s & len p <= len r ) ; :: thesis: ex t, u being FinSequence st
( p ^ t = r & u ^ s = q )
then (len r) - (len p) in NAT by INT_1:5;
then reconsider k = (len r) - (len p) as Nat ;
A3: (len p) + (len q) = len (p ^ q) by FINSEQ_1:22
.= (len r) + (len s) by A1, FINSEQ_1:22 ;
then len q = k + (len s) ;
then A5: len q >= k + 0 by XREAL_1:6;
A6: len (p ^ (q | k)) = (len p) + (len (q | k)) by FINSEQ_1:22
.= (len p) + k by A5, FINSEQ_1:59
.= len r ;
A7: len ((r /^ (len p)) ^ s) = (len (r /^ (len p))) + (len s) by FINSEQ_1:22
.= ((len r) - (len p)) + (len s) by A1, Def1
.= len q by A3 ;
take q | k ; :: thesis: ex u being FinSequence st
( p ^ (q | k) = r & u ^ s = q )
take r /^ (len p) ; :: thesis: ( p ^ (q | k) = r & (r /^ (len p)) ^ s = q )

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

let i be Nat; :: thesis: ( 1 <= i & i <= len r implies (p ^ (q | k)) . b₁ = r . b₁ )
assume A8: ( 1 <= i & i <= len r ) ; :: thesis: (p ^ (q | k)) . b₁ = r . b₁
then A9: i in dom r by FINSEQ_3:25;

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

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

then A11: i in dom p by A8, FINSEQ_3:25;
hence (p ^ (q | k)) . i = p . i by FINSEQ_1:def 7
.= (r ^ s) . i by A1, A11, FINSEQ_1:def 7
.= r . i by A9, FINSEQ_1:def 7 ;
:: thesis: verum

end;

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

then (len p) + 1 <= i by NAT_1:13;
then consider j being Nat such that
A14: i = ((len p) + 1) + j by NAT_1:10;
A15: i = (len p) + (1 + j) by A14;
(len p) + (1 + j) <= (len p) + k by A8, A14;
then 1 + j <= k by XREAL_1:6;
then A16: 1 + j <= len (q | k) by A5, FINSEQ_1:59;
1 + 0 <= 1 + j by XREAL_1:6;
then A17: 1 + j in dom (q | k) by A16, FINSEQ_3:25;
then A18: 1 + j in dom (q | (Seg k)) ;
then A19: 1 + j in dom q by RELAT_1:60, TARSKI:def 3;
thus (p ^ (q | k)) . i = (q | k) . (1 + j) by A15, A17, FINSEQ_1:def 7
.= (q | (Seg k)) . (1 + j)
.= q . (1 + j) by A18, FUNCT_1:47
.= (r ^ s) . i by A1, A15, A19, FINSEQ_1:def 7
.= r . i by A9, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence p ^ (q | k) = r by A6, FINSEQ_1:14; :: thesis: (r /^ (len p)) ^ s = q

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

let i be Nat; :: thesis: ( 1 <= i & i <= len q implies ((r /^ (len p)) ^ s) . b₁ = q . b₁ )
assume A20: ( 1 <= i & i <= len q ) ; :: thesis: ((r /^ (len p)) ^ s) . b₁ = q . b₁
then A21: i in dom q by FINSEQ_3:25;

per cases ( i <= k or k < i ) ;

suppose A22: i <= k ; :: thesis: ((r /^ (len p)) ^ s) . b₁ = q . b₁

len (r /^ (len p)) = k by A1, Def1;
then A25: i in dom (r /^ (len p)) by A20, A22, FINSEQ_3:25;
A26: i + (len p) <= ((len r) - (len p)) + (len p) by A22, XREAL_1:6;
1 + 0 <= i + (len p) by A20, XREAL_1:7;
then A27: i + (len p) in dom r by A26, FINSEQ_3:25;
thus ((r /^ (len p)) ^ s) . i = (r /^ (len p)) . i by A25, FINSEQ_1:def 7
.= r . (i + (len p)) by A1, A25, Def1
.= (p ^ q) . ((len p) + i) by A1, A27, FINSEQ_1:def 7
.= q . i by A21, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose k < i ; :: thesis: ((r /^ (len p)) ^ s) . b₁ = q . b₁

then k + 1 <= i by NAT_1:13;
then consider j being Nat such that
A29: i = (k + 1) + j by NAT_1:10;
len (r /^ (len p)) = k by A1, Def1;
then A30: i = (len (r /^ (len p))) + (1 + j) by A29;
i <= (len (r /^ (len p))) + (len s) by A7, A20, FINSEQ_1:22;
then A31: 1 + j <= len s by A30, XREAL_1:6;
1 + 0 <= 1 + j by XREAL_1:6;
then A32: 1 + j in dom s by A31, FINSEQ_3:25;
thus ((r /^ (len p)) ^ s) . i = s . (1 + j) by A30, A32, FINSEQ_1:def 7
.= (p ^ q) . ((len r) + (1 + j)) by A1, A32, FINSEQ_1:def 7
.= (p ^ q) . ((len p) + i) by A29
.= q . i by A21, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence (r /^ (len p)) ^ s = q by A7, FINSEQ_1:14; :: thesis: verum