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 that
A1: 1 <= k1 and
A2: 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;
A3: len (f | k21) = k21 by A2, Th12;
k1 < k1 + 1 by NAT_1:13;
then k1 - 1 < (k1 + 1) - 1 by XREAL_1:11;
then A4: k1 -' 1 < k1 by A1, XREAL_1:235;
A5: mid f,k1,k2 = (f | k21) /^ (k11 -' 1) by Def3;

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

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

A7: k2 < k2 + 1 by XREAL_1:31;
then A8: (k2 + 1) -' k1 = (k2 + 1) - k1 by A6, XREAL_1:235, XXREAL_0:2
.= k2 - (k1 - 1) ;
A9: k11 -' 1 = k11 - 1 by A1, XREAL_1:235;
k11 - 1 < k11 by XREAL_1:46;
then k11 - 1 < k21 by A6, XXREAL_0:2;
then A10: len (mid f,k1,k2) = k21 - (k11 - 1) by A5, A3, A9, Th16;
then A11: len (mid f,k1,k2) = (k21 + 1) - k11 ;
k1 -' 1 < k2 by A4, A6, XXREAL_0:2;
then k1 -' 1 < len f by A2, XXREAL_0:2;
then len (f /^ (k1 -' 1)) = (len f) - (k1 -' 1) by Th16;
then A12: (k2 + 1) -' k1 <= len (f /^ (k1 -' 1)) by A2, A9, A8, XREAL_1:11;
A13: 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 A14: 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 A9, A10, XREAL_1:22;
then A15: i + (k11 -' 1) in k21 by NAT_1:45;
i + (k1 -' 1) < (k21 - (k11 - 1)) + (k1 -' 1) by A10, A14, XREAL_1:8;
then A16: i + (k1 -' 1) < len f by A2, A9, XXREAL_0:2;
i + (k11 - 1) < k21 by A10, A14, XREAL_1:22;
then A17: ((f | k21) /^ (k11 -' 1)) . i = (f | k21) . (i + (k11 -' 1)) by A3, A9, Th17;
i in (k2 + 1) -' k1 by A8, A10, A14, NAT_1:45;
then ((f /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i = (f /^ (k1 -' 1)) . i by A12, Th11
.= f . (i + (k1 -' 1)) by A16, Th17 ;
hence (mid f,k1,k2) . i = ((f /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i by A2, A5, A17, A15, Th11; :: thesis: verum

end;

len ((f /^ (k1 -' 1)) | ((k2 + 1) -' k1)) = (k2 + 1) -' k1 by A12, Th12;
then len (mid f,k1,k2) = len ((f /^ (k1 -' 1)) | ((k2 + 1) -' k1)) by A6, A7, A11, XREAL_1:235, XXREAL_0:2;
hence mid f,k1,k2 = (f /^ (k1 -' 1)) | ((k2 + 1) -' k1) by A13, AFINSQ_1:11; :: thesis: verum

end;

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

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

end;

end;