let f be FinSequence; :: thesis: for k1, k2 being Nat holds len (mid (f,k1,k2)) <= len f
let k1, k2 be Nat; :: thesis: len (mid (f,k1,k2)) <= len f

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

suppose k1 <= k2 ; :: thesis: len (mid (f,k1,k2)) <= len f

then A1: mid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) by Def3;

per cases ( len (f /^ (k1 -' 1)) <= (k2 -' k1) + 1 or len (f /^ (k1 -' 1)) > (k2 -' k1) + 1 ) ;

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

then A2: mid (f,k1,k2) = f /^ (k1 -' 1) by A1, FINSEQ_1:58;

per cases ( k1 -' 1 <= len f or not k1 -' 1 <= len f ) ;

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

(len f) - (k1 -' 1) <= (len f) - 0 by XREAL_1:10;
hence len (mid (f,k1,k2)) <= len f by A2, A3, RFINSEQ:def 1; :: thesis: verum

end;

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

then f /^ (k1 -' 1) = {} by RFINSEQ:def 1;
hence len (mid (f,k1,k2)) <= len f by A2; :: thesis: verum

end;

end;

end;

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

then A5: len (mid (f,k1,k2)) <= len (f /^ (k1 -' 1)) by A1, FINSEQ_1:59;

per cases ( k1 -' 1 <= len f or not k1 -' 1 <= len f ) ;

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

then A6: len (mid (f,k1,k2)) <= (len f) - (k1 -' 1) by A5, RFINSEQ:def 1;
(len f) - (k1 -' 1) <= (len f) - 0 by XREAL_1:10;
hence len (mid (f,k1,k2)) <= len f by A6, XXREAL_0:2; :: thesis: verum

end;

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

then f /^ (k1 -' 1) = {} by RFINSEQ:def 1;
hence len (mid (f,k1,k2)) <= len f by A5; :: thesis: verum

end;

end;

end;

end;

end;

suppose k1 > k2 ; :: thesis: len (mid (f,k1,k2)) <= len f

then A7: mid (f,k1,k2) = Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) by Def3;
set m = (f /^ (k2 -' 1)) | ((k1 -' k2) + 1);
len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f

proof

per cases ( len (f /^ (k2 -' 1)) <= (k1 -' k2) + 1 or len (f /^ (k2 -' 1)) > (k1 -' k2) + 1 ) ;

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

then A8: (f /^ (k2 -' 1)) | ((k1 -' k2) + 1) = f /^ (k2 -' 1) by FINSEQ_1:58;

per cases ( k2 -' 1 <= len f or not k2 -' 1 <= len f ) ;

suppose A9: k2 -' 1 <= len f ; :: thesis: len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f

(len f) - (k2 -' 1) <= (len f) - 0 by XREAL_1:10;
hence len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f by A8, A9, RFINSEQ:def 1; :: thesis: verum

end;

suppose not k2 -' 1 <= len f ; :: thesis: len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f

then f /^ (k2 -' 1) = {} by RFINSEQ:def 1;
hence len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f ; :: thesis: verum

end;

end;

end;

suppose len (f /^ (k2 -' 1)) > (k1 -' k2) + 1 ; :: thesis: len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f

then A11: len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len (f /^ (k2 -' 1)) by FINSEQ_1:59;

per cases ( k2 -' 1 <= len f or not k2 -' 1 <= len f ) ;

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

then A12: len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= (len f) - (k2 -' 1) by A11, RFINSEQ:def 1;
(len f) - (k2 -' 1) <= (len f) - 0 by XREAL_1:10;
hence len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f by A12, XXREAL_0:2; :: thesis: verum

end;

suppose not k2 -' 1 <= len f ; :: thesis: len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f

then f /^ (k2 -' 1) = {} by RFINSEQ:def 1;
hence len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f ; :: thesis: verum

end;

end;

end;

end;

end;

hence len (mid (f,k1,k2)) <= len f by A7, FINSEQ_5:def 3; :: thesis: verum

end;

end;