let D be non empty set ; :: thesis: for f being FinSequence of D
for k1, k2, k3 being Element of 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 Element of 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 Element of 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:124
.= (k2 - k1) + 1 by A3, XREAL_1:235 ;
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:124
.= (k3 - (k2 + 1)) + 1 by A12, XREAL_1:235
.= k3 - k2 ;
then A14: len ((mid f,k1,k2) ^ (mid f,(k2 + 1),k3)) = ((k2 - k1) + 1) + (k3 - k2) by A7, FINSEQ_1:35
.= (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:3;
then A18: k in dom ((mid f,k1,k2) ^ (mid f,(k2 + 1),k3)) by FINSEQ_1:def 3;

now

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:38;

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:3;
A22: k <= (k2 - k1) + 1 by A7, A20, FINSEQ_1:3;
k2 - k1 <= k3 - k1 by A4, XREAL_1:11;
then (k2 - k1) + 1 <= (k3 - k1) + 1 by XREAL_1:8;
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, A19, A21, A22, FINSEQ_6:128 ;
hence ((mid f,k1,k2) ^ (mid f,(k2 + 1),k3)) . k = (mid f,k1,k3) . k by A1, A2, A10, A19, A21, A23, FINSEQ_6:128; :: 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:128
.= 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:3;
((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, A24, A27, FINSEQ_6:128
.= 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:124
.= (k3 - k1) + 1 by A3, A4, XREAL_1:235, XXREAL_0:2 ;
hence (mid f,k1,k2) ^ (mid f,(k2 + 1),k3) = mid f,k1,k3 by A14, A16, FINSEQ_1:18; :: thesis: verum