let p be FinSequence; :: thesis: for m, n being Element of NAT holds rng (m,n -cut p) c= rng p
let m, n be Element of NAT ; :: thesis: rng (m,n -cut p) c= rng p
set c = m,n -cut p;

A1: now

assume that
A2: 1 <= m and
A3: m <= n and
A4: n <= len p ; :: thesis: rng (m,n -cut p) c= rng p
n <= n + 1 by NAT_1:11;
then A5: m <= n + 1 by A3, XXREAL_0:2;
thus rng (m,n -cut p) c= rng p :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (m,n -cut p) or x in rng p )
assume x in rng (m,n -cut p) ; :: thesis: x in rng p
then consider z being set such that
A6: ( z in dom (m,n -cut p) & x = (m,n -cut p) . z ) by FUNCT_1:def 5;
reconsider z = z as Element of NAT by A6;
( 0 + 1 <= z & z <= len (m,n -cut p) ) by A6, FINSEQ_3:27;
then consider i being Element of NAT such that
A7: ( 0 <= i & i < len (m,n -cut p) & z = i + 1 ) by Th1;
A8: (m,n -cut p) . z = p . (m + i) by A2, A4, A5, A7, Lm2;
m + i < (len (m,n -cut p)) + m by A7, XREAL_1:8;
then m + i < n + 1 by A2, A4, A5, Lm2;
then m + i <= n by NAT_1:13;
then ( 1 <= m + i & m + i <= len p ) by A2, A4, NAT_1:12, XXREAL_0:2;
then m + i in dom p by FINSEQ_3:27;
hence x in rng p by A6, A8, FUNCT_1:def 5; :: thesis: verum

end;

end;

now

assume ( not 1 <= m or not m <= n or not n <= len p ) ; :: thesis: rng (m,n -cut p) c= rng p
then m,n -cut p = {} by Def1;
then rng (m,n -cut p) = {} ;
hence rng (m,n -cut p) c= rng p by XBOOLE_1:2; :: thesis: verum

end;

hence rng (m,n -cut p) c= rng p by A1; :: thesis: verum