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