let p be XFinSequence; :: thesis: for k1, k2 being Nat st 1 <= k1 & k2 <= len p holds
mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1)
let k1, k2 be Nat; :: thesis: ( 1 <= k1 & k2 <= len p implies mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1) )
assume that
A1: 1 <= k1 and
A2: k2 <= len p ; :: thesis: mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1)
set k11 = k1;
set k21 = k2;
A3: len (p | k2) = k2 by A2, AFINSQ_1:54;
k1 < k1 + 1 by NAT_1:13;
then k1 - 1 < (k1 + 1) - 1 by XREAL_1:9;
then A4: k1 -' 1 < k1 by A1, XREAL_1:233;

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

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

A6: k2 < k2 + 1 by XREAL_1:29;
then A7: (k2 + 1) -' k1 = (k2 + 1) - k1 by A5, XREAL_1:233, XXREAL_0:2
.= k2 - (k1 - 1) ;
A8: k1 -' 1 = k1 - 1 by A1, XREAL_1:233;
k1 - 1 < k1 by XREAL_1:44;
then k1 - 1 < k2 by A5, XXREAL_0:2;
then A9: len (mid (p,k1,k2)) = k2 - (k1 - 1) by A3, A8, Th7;
then A10: len (mid (p,k1,k2)) = (k2 + 1) - k1 ;
k1 -' 1 < k2 by A4, A5, XXREAL_0:2;
then k1 -' 1 < len p by A2, XXREAL_0:2;
then len (p /^ (k1 -' 1)) = (len p) - (k1 -' 1) by Th7;
then A11: (k2 + 1) -' k1 <= len (p /^ (k1 -' 1)) by A2, A8, A7, XREAL_1:9;
A12: for i being Nat st i < len (mid (p,k1,k2)) holds
(mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i

proof

let i be Nat; :: thesis: ( i < len (mid (p,k1,k2)) implies (mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i )
assume A13: i < len (mid (p,k1,k2)) ; :: thesis: (mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i
then A14: i + (k1 -' 1) in Segm k2 by NAT_1:44, A8, A9, XREAL_1:20;
i + (k1 -' 1) < (k2 - (k1 - 1)) + (k1 -' 1) by A9, A13, XREAL_1:6;
then A15: i + (k1 -' 1) < len p by A2, A8, XXREAL_0:2;
i + (k1 - 1) < k2 by A9, A13, XREAL_1:20;
then A16: ((p | k2) /^ (k1 -' 1)) . i = (p | k2) . (i + (k1 -' 1)) by A3, A8, Th8;
i in (k2 + 1) -' k1 by A7, A9, A13, AFINSQ_1:86;
then ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i = (p /^ (k1 -' 1)) . i by A11, AFINSQ_1:53
.= p . (i + (k1 -' 1)) by A15, Th8 ;
hence (mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i by A2, A16, A14, AFINSQ_1:53; :: thesis: verum

end;

len ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) = (k2 + 1) -' k1 by A11, AFINSQ_1:54;
then len (mid (p,k1,k2)) = len ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) by A5, A6, A10, XREAL_1:233, XXREAL_0:2;
hence mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1) by A12, AFINSQ_1:9; :: thesis: verum

end;

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

then k2 + 1 <= k1 by NAT_1:13;
then A18: (k2 + 1) -' k1 = 0 by NAT_2:8;
mid (p,k1,k2) = {} by A17, Th14;
hence mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1) by A18; :: thesis: verum

end;

end;