let f be FinSequence; :: thesis: for k1, k2 being Nat st k1 in dom f & k2 in dom f holds
smid (f,k1,k2) = (k1,k2) -cut f
let k1, k2 be Nat; :: thesis: ( k1 in dom f & k2 in dom f implies smid (f,k1,k2) = (k1,k2) -cut f )
set ff = (k1,k2) -cut f;
set g = smid (f,k1,k2);
reconsider af = f as FinSequence of rng f by FINSEQ_1:def 4;
assume ( k1 in dom f & k2 in dom f ) ; :: thesis: smid (f,k1,k2) = (k1,k2) -cut f
then S0: ( 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f ) by FINSEQ_3:25;

per cases ( k1 <= k2 or k1 > k2 ) ;

suppose A0: k1 <= k2 ; :: thesis: smid (f,k1,k2) = (k1,k2) -cut f

then WW: smid (f,k1,k2) = mid (f,k1,k2) by Th4;
(len ((k1,k2) -cut f)) + k1 = k2 + 1 by A0, S0, FINSEQ_6:def 4;
then S2: len ((k1,k2) -cut f) = (k2 + 1) - k1
.= (k2 + 1) -' k1 by A0, NAT_D:37 ;
k2 <= k2 + 1 by NAT_1:13;
then W4: (k2 + 1) - k1 = (k2 + 1) -' k1 by XREAL_1:233, A0, XXREAL_0:2;
k1 -' 1 <= k1 by NAT_D:35;
then k1 -' 1 <= len f by XXREAL_0:2, S0;
then S3: len (f /^ (k1 -' 1)) = (len f) - (k1 -' 1) by RFINSEQ:def 1;
W3: (len f) - (k1 -' 1) = (len f) - (k1 - 1) by S0, XREAL_1:233
.= ((len f) + 1) - k1 ;
k2 + 1 <= (len f) + 1 by S0, XREAL_1:6;
then (k2 + 1) -' k1 <= len (f /^ (k1 -' 1)) by S3, W3, W4, XREAL_1:9;
then A1: len ((k1,k2) -cut f) = len (smid (f,k1,k2)) by S2, FINSEQ_1:59;
for k being Nat st 1 <= k & k <= len ((k1,k2) -cut f) holds
((k1,k2) -cut f) . k = (smid (f,k1,k2)) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len ((k1,k2) -cut f) implies ((k1,k2) -cut f) . k = (smid (f,k1,k2)) . k )
assume Z0: ( 1 <= k & k <= len ((k1,k2) -cut f) ) ; :: thesis: ((k1,k2) -cut f) . k = (smid (f,k1,k2)) . k
then ZZ: (k -' 1) + 1 = k by XREAL_1:235;
k -' 1 < len ((k1,k2) -cut f)

proof

per cases ( k > 1 or k = 1 ) by Z0, XXREAL_0:1;

suppose k > 1 ; :: thesis: k -' 1 < len ((k1,k2) -cut f)

then 1 <= k -' 1 by NAT_D:49;
then k -' 1 < k by NAT_D:51;
hence k -' 1 < len ((k1,k2) -cut f) by Z0, XXREAL_0:2; :: thesis: verum

end;

suppose k = 1 ; :: thesis: k -' 1 < len ((k1,k2) -cut f)

then k -' 1 < k by NAT_D:51;
hence k -' 1 < len ((k1,k2) -cut f) by Z0, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then Z2: ((k1,k2) -cut f) . k = f . (k1 + (k -' 1)) by ZZ, FINSEQ_6:def 4, A0, S0;
P1: k <= len (mid (af,k1,k2)) by WW, A1, Z0;
k1 + k >= k by NAT_1:11;
then P2: 1 <= k1 + k by XXREAL_0:2, Z0;
(smid (f,k1,k2)) . k = (mid (f,k1,k2)) . k by Th4, A0
.= af . ((k + k1) -' 1) by Z0, FINSEQ_6:118, A0, P1, S0
.= af . ((k1 + k) - 1) by P2, XREAL_1:233
.= af . (k1 + (k - 1))
.= af . (k1 + (k -' 1)) by Z0, XREAL_1:233 ;
hence ((k1,k2) -cut f) . k = (smid (f,k1,k2)) . k by Z2; :: thesis: verum

end;

hence smid (f,k1,k2) = (k1,k2) -cut f by A1; :: thesis: verum

end;

suppose A1: k1 > k2 ; :: thesis: smid (f,k1,k2) = (k1,k2) -cut f

then (k1,k2) -cut f = {} by FINSEQ_6:def 4;
hence smid (f,k1,k2) = (k1,k2) -cut f by A1, Th7; :: thesis: verum

end;

end;