let m, n be Nat; :: thesis: for f being FinSequence holds len ((m,n) -cut f) <= len f
let f be FinSequence; :: thesis: len ((m,n) -cut f) <= len f
set lmnf = len ((m,n) -cut f);
set lf = len f;

per cases ( ( 1 <= m & m <= n & n <= len f ) or not 1 <= m or not m <= n or not n <= len f ) ;

suppose A1: ( 1 <= m & m <= n & n <= len f ) ; :: thesis: len ((m,n) -cut f) <= len f

then (len ((m,n) -cut f)) + m = n + 1 by FINSEQ_6:def 4;
then n + ((len ((m,n) -cut f)) + m) <= (n + 1) + (len f) by A1, XREAL_1:6;
then n + ((len ((m,n) -cut f)) + m) <= n + (1 + (len f)) ;
then (len ((m,n) -cut f)) + m <= 1 + (len f) by XREAL_1:6;
then ((len ((m,n) -cut f)) + m) + 1 <= m + (1 + (len f)) by A1, XREAL_1:7;
then (len ((m,n) -cut f)) + (m + 1) <= (m + 1) + (len f) ;
hence len ((m,n) -cut f) <= len f by XREAL_1:6; :: thesis: verum

end;

suppose ( not 1 <= m or not m <= n or not n <= len f ) ; :: thesis: len ((m,n) -cut f) <= len f

then (m,n) -cut f is empty by FINSEQ_6:def 4;
hence len ((m,n) -cut f) <= len f ; :: thesis: verum

end;

end;