let m, n be Nat; :: thesis: for f being non empty FinSequence st 1 <= m & m <= n & n <= len f holds
not (m,n) -cut f is empty
let f be non empty FinSequence; :: thesis: ( 1 <= m & m <= n & n <= len f implies not (m,n) -cut f is empty )
set lmn = len ((m,n) -cut f);
assume ( 1 <= m & m <= n & n <= len f ) ; :: thesis: not (m,n) -cut f is empty
then ( m < n + 1 & (len ((m,n) -cut f)) + m = n + 1 ) by FINSEQ_6:def 4, NAT_1:13;
then m - ((len ((m,n) -cut f)) + m) < (n + 1) - (n + 1) by XREAL_1:9;
then - (- (len ((m,n) -cut f))) > 0 ;
hence not (m,n) -cut f is empty ; :: thesis: verum