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 A1: ( 1 <= k1 & k3 <= len f & k1 <= k2 & k2 < k3 ) ; :: thesis: (mid f,k1,k2) ^ (mid f,(k2 + 1),k3) = mid f,k1,k3
then A2: ( 1 <= k2 & k2 <= len f ) by XXREAL_0:2;
then A3: ( 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & 1 <= k3 & k3 <= len f & k1 <= k2 & k2 < k3 ) by A1, XXREAL_0:2;
A4: ( 1 <= k2 + 1 & k2 + 1 <= k3 & k1 < k3 ) by A1, A2, NAT_1:13, XXREAL_0:2;
then A5: ( 1 <= k2 + 1 & k2 + 1 <= k3 & k2 + 1 <= len f & k1 <= k3 & k1 <= k2 + 1 ) by A1, NAT_1:12, XXREAL_0:2;
A6: len (mid f,k1,k2) = (k2 -' k1) + 1 by A3, JORDAN3:27
.= (k2 - k1) + 1 by A1, XREAL_1:235 ;
A7: len (mid f,(k2 + 1),k3) = (k3 -' (k2 + 1)) + 1 by A3, A5, JORDAN3:27
.= (k3 - (k2 + 1)) + 1 by A4, XREAL_1:235
.= k3 - k2 ;
then A8: len ((mid f,k1,k2) ^ (mid f,(k2 + 1),k3)) = ((k2 - k1) + 1) + (k3 - k2) by A6, FINSEQ_1:35
.= (k3 - k1) + 1 ;
A9: len (mid f,k1,k3) = (k3 -' k1) + 1 by A3, A4, JORDAN3:27
.= (k3 - k1) + 1 by A4, XREAL_1:235 ;
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 A10: ( 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 A11: 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 A11, FINSEQ_1:38;

suppose A12: k in dom (mid f,k1,k2) ; :: 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)) by FINSEQ_1:def 3;
then A13: ( 1 <= k & k <= (k2 - k1) + 1 ) by A6, FINSEQ_1:3;
k2 - k1 <= k3 - k1 by A1, XREAL_1:11;
then (k2 - k1) + 1 <= (k3 - k1) + 1 by XREAL_1:8;
then A14: k <= (k3 - k1) + 1 by A13, XXREAL_0:2;
((mid f,k1,k2) ^ (mid f,(k2 + 1),k3)) . k = (mid f,k1,k2) . k by A12, FINSEQ_1:def 7
.= f . ((k - 1) + k1) by A1, A2, A12, A13, JORDAN3:31 ;
hence ((mid f,k1,k2) ^ (mid f,(k2 + 1),k3)) . k = (mid f,k1,k3) . k by A1, A4, A12, A13, A14, JORDAN3:31; :: 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
A15: ( n in dom (mid f,(k2 + 1),k3) & k = (len (mid f,k1,k2)) + n ) ;
n in Seg (len (mid f,(k2 + 1),k3)) by A15, FINSEQ_1:def 3;
then A16: ( 1 <= n & n <= (k3 - (k2 + 1)) + 1 ) by A7, FINSEQ_1:3;
A17: ((mid f,k1,k2) ^ (mid f,(k2 + 1),k3)) . k = (mid f,(k2 + 1),k3) . n by A15, FINSEQ_1:def 7
.= f . ((n + (k2 + 1)) - 1) by A1, A4, A15, A16, JORDAN3:31
.= f . ((n + k2) + 0 ) ;
(mid f,k1,k3) . k = f . ((((k2 - (k1 - 1)) + n) + k1) - 1) by A1, A4, A6, A8, A10, A15, JORDAN3:31
.= f . (n + k2) ;
hence ((mid f,k1,k2) ^ (mid f,(k2 + 1),k3)) . k = (mid f,k1,k3) . k by A17; :: thesis: verum

end;

end;

end;

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

end;

hence (mid f,k1,k2) ^ (mid f,(k2 + 1),k3) = mid f,k1,k3 by A8, A9, FINSEQ_1:18; :: thesis: verum