let D be non empty set ; :: thesis: for f being FinSequence of D
for k1, k2, k3 being Nat st 1 <= k1 & k3 <= len f & k1 <= k2 & k2 < k3 holds
(mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3)
let f be FinSequence of D; :: thesis: for k1, k2, k3 being Nat st 1 <= k1 & k3 <= len f & k1 <= k2 & k2 < k3 holds
(mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3)
let k1, k2, k3 be Nat; :: thesis: ( 1 <= k1 & k3 <= len f & k1 <= k2 & k2 < k3 implies (mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3) )
assume that
A1: 1 <= k1 and
A2: k3 <= len f and
A3: k1 <= k2 and
A4: k2 < k3 ; :: thesis: (mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3)
A5: k2 <= len f by A2, A4, XXREAL_0:2;
then A6: k1 <= len f by A3, XXREAL_0:2;
( 1 <= k2 & k2 <= len f ) by A1, A2, A3, A4, XXREAL_0:2;
then A7: len (mid (f,k1,k2)) = (k2 -' k1) + 1 by A1, A3, A6, FINSEQ_6:118
.= (k2 - k1) + 1 by A3, XREAL_1:233 ;
A8: 1 <= k2 by A1, A3, XXREAL_0:2;
then A9: 1 <= k3 by A4, XXREAL_0:2;
A10: k1 < k3 by A3, A4, XXREAL_0:2;
A11: 1 <= k2 + 1 by A8, NAT_1:13;
A12: k2 + 1 <= k3 by A4, NAT_1:13;
then k2 + 1 <= len f by A2, XXREAL_0:2;
then A13: len (mid (f,(k2 + 1),k3)) = (k3 -' (k2 + 1)) + 1 by A2, A9, A12, A11, FINSEQ_6:118
.= (k3 - (k2 + 1)) + 1 by A12, XREAL_1:233
.= k3 - k2 ;
then A14: len ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) = ((k2 - k1) + 1) + (k3 - k2) by A7, FINSEQ_1:22
.= (k3 - k1) + 1 ;
A15: 1 <= k2 + 1 by A8, NAT_1:13;
A16: for k being Nat st 1 <= k & k <= len ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) holds
((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) implies ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k )
assume A17: ( 1 <= k & k <= len ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) ) ; :: thesis: ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k
then k in Seg (len ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)))) by FINSEQ_1:1;
then A18: k in dom ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) by FINSEQ_1:def 3;

now :: thesis: ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k

per cases ( k in dom (mid (f,k1,k2)) or ex n being Nat st
( n in dom (mid (f,(k2 + 1),k3)) & k = (len (mid (f,k1,k2))) + n ) ) by A18, FINSEQ_1:25;

suppose A19: k in dom (mid (f,k1,k2)) ; :: thesis: ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k

then A20: k in Seg (len (mid (f,k1,k2))) by FINSEQ_1:def 3;
then A21: 1 <= k by FINSEQ_1:1;
A22: k <= (k2 - k1) + 1 by A7, A20, FINSEQ_1:1;
k2 - k1 <= k3 - k1 by A4, XREAL_1:9;
then (k2 - k1) + 1 <= (k3 - k1) + 1 by XREAL_1:6;
then A23: k <= (k3 - k1) + 1 by A22, XXREAL_0:2;
((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k2)) . k by A19, FINSEQ_1:def 7
.= f . ((k - 1) + k1) by A1, A3, A5, A21, A22, FINSEQ_6:122 ;
hence ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k by A1, A2, A10, A21, A23, FINSEQ_6:122; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom (mid (f,(k2 + 1),k3)) & k = (len (mid (f,k1,k2))) + n ) ; :: thesis: ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k

then consider n being Nat such that
A24: n in dom (mid (f,(k2 + 1),k3)) and
A25: k = (len (mid (f,k1,k2))) + n ;
A26: (mid (f,k1,k3)) . k = f . ((((k2 - (k1 - 1)) + n) + k1) - 1) by A1, A2, A10, A7, A14, A17, A25, FINSEQ_6:122
.= f . (n + k2) ;
n in Seg (len (mid (f,(k2 + 1),k3))) by A24, FINSEQ_1:def 3;
then A27: ( 1 <= n & n <= (k3 - (k2 + 1)) + 1 ) by A13, FINSEQ_1:1;
((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,(k2 + 1),k3)) . n by A24, A25, FINSEQ_1:def 7
.= f . ((n + (k2 + 1)) - 1) by A2, A15, A12, A27, FINSEQ_6:122
.= f . ((n + k2) + 0) ;
hence ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k by A26; :: thesis: verum

end;

end;

end;

hence ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k ; :: thesis: verum

end;

len (mid (f,k1,k3)) = (k3 -' k1) + 1 by A1, A2, A6, A9, A10, FINSEQ_6:118
.= (k3 - k1) + 1 by A3, A4, XREAL_1:233, XXREAL_0:2 ;
hence (mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3) by A14, A16, FINSEQ_1:14; :: thesis: verum