let m, n be Element of 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 GRAPH_2:def 1, NAT_1:13;
then m - ((len ((m,n) -cut f)) + m) < (n + 1) - (n + 1) by XREAL_1:11;
then - (- (len ((m,n) -cut f))) > 0 ;
hence not (m,n) -cut f is empty ; :: thesis: verum