let f be XFinSequence; :: thesis: for k1, k2 being Nat st 1 <= k1 & k2 <= len f holds
mid f,k1,k2 = (f /^ (k1 -' 1)) | ((k2 + 1) -' k1)
let k1, k2 be Nat; :: thesis: ( 1 <= k1 & k2 <= len f implies mid f,k1,k2 = (f /^ (k1 -' 1)) | ((k2 + 1) -' k1) )
assume A5: ( 1 <= k1 & k2 <= len f ) ; :: thesis: mid f,k1,k2 = (f /^ (k1 -' 1)) | ((k2 + 1) -' k1)
reconsider k11 = k1, k21 = k2 as Element of NAT by ORDINAL1:def 13;
A2: mid f,k1,k2 = (f | k21) /^ (k11 -' 1) by AB540b;
B2: len (f | k21) = k21 by TH80, A5;
k1 < k1 + 1 by NAT_1:13;
then k1 - 1 < (k1 + 1) - 1 by XREAL_1:11;
then B43: k1 -' 1 < k1 by A5, XREAL_1:235;

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

suppose A6: k1 <= k2 ; :: thesis: mid f,k1,k2 = (f /^ (k1 -' 1)) | ((k2 + 1) -' k1)

B9: k2 < k2 + 1 by XREAL_1:31;
B7: k11 -' 1 = k11 - 1 by A5, XREAL_1:235;
k1 -' 1 < k2 by A6, B43, XXREAL_0:2;
then k1 -' 1 < len f by A5, XXREAL_0:2;
then B20: len (f /^ (k1 -' 1)) = (len f) - (k1 -' 1) by TH80b;
B21: (k2 + 1) -' k1 = (k2 + 1) - k1 by B9, A6, XREAL_1:235, XXREAL_0:2
.= k2 - (k1 - 1) ;
then B30: (k2 + 1) -' k1 <= len (f /^ (k1 -' 1)) by B20, A5, B7, XREAL_1:11;
then B5: len ((f /^ (k1 -' 1)) | ((k2 + 1) -' k1)) = (k2 + 1) -' k1 by TH80;
k11 - 1 < k11 by XREAL_1:46;
then k11 - 1 < k21 by A6, XXREAL_0:2;
then B3: len (mid f,k1,k2) = k21 - (k11 - 1) by TH80b, A2, B2, B7;
then len (mid f,k1,k2) = (k21 + 1) - k11 ;
then B10: len (mid f,k1,k2) = len ((f /^ (k1 -' 1)) | ((k2 + 1) -' k1)) by B5, B9, A6, XREAL_1:235, XXREAL_0:2;
for i being Element of NAT st i < len (mid f,k1,k2) holds
(mid f,k1,k2) . i = ((f /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i

proof

let i be Element of NAT ; :: thesis: ( i < len (mid f,k1,k2) implies (mid f,k1,k2) . i = ((f /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i )
assume C2: i < len (mid f,k1,k2) ; :: thesis: (mid f,k1,k2) . i = ((f /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i
then i + (k11 - 1) < k21 by B3, XREAL_1:22;
then C12: ((f | k21) /^ (k11 -' 1)) . i = (f | k21) . (i + (k11 -' 1)) by B2, B7, Th19b;
i + (k11 -' 1) < k21 by C2, B3, B7, XREAL_1:22;
then C40: i + (k11 -' 1) in k21 by NAT_1:45;
i + (k1 -' 1) < (k21 - (k11 - 1)) + (k1 -' 1) by C2, B3, XREAL_1:8;
then C10: i + (k1 -' 1) < len f by A5, B7, XXREAL_0:2;
C9: i in (k2 + 1) -' k1 by C2, B3, B21, NAT_1:45;
((f /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i = (f /^ (k1 -' 1)) . i by Th19, C9, B30
.= f . (i + (k1 -' 1)) by Th19b, C10 ;
hence (mid f,k1,k2) . i = ((f /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i by C40, Th19, A5, A2, C12; :: thesis: verum

end;

hence mid f,k1,k2 = (f /^ (k1 -' 1)) | ((k2 + 1) -' k1) by B10, AFINSQ_1:11; :: thesis: verum

end;

suppose A6: k1 > k2 ; :: thesis: mid f,k1,k2 = (f /^ (k1 -' 1)) | ((k2 + 1) -' k1)

then D3: mid f,k1,k2 = {} by AB540f;
k2 + 1 <= k1 by A6, NAT_1:13;
then (k2 + 1) -' k1 = 0 by NAT_2:10;
hence mid f,k1,k2 = (f /^ (k1 -' 1)) | ((k2 + 1) -' k1) by D3; :: thesis: verum

end;

end;