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) and
A7: x = (m,n -cut p) . z by FUNCT_1:def 5;
reconsider z = z as Element of NAT by A6;
A8: z <= len (m,n -cut p) by A6, FINSEQ_3:27;
0 + 1 <= z by A6, FINSEQ_3:27;
then consider i being Element of NAT such that
0 <= i and
A9: i < len (m,n -cut p) and
A10: z = i + 1 by A8, Th1;
m + i < (len (m,n -cut p)) + m by A9, XREAL_1:8;
then m + i < n + 1 by A2, A4, A5, Lm2;
then m + i <= n by NAT_1:13;
then A11: m + i <= len p by A4, XXREAL_0:2;
1 <= m + i by A2, NAT_1:12;
then A12: m + i in dom p by A11, FINSEQ_3:27;
(m,n -cut p) . z = p . (m + i) by A2, A4, A5, A9, A10, Lm2;
hence x in rng p by A7, A12, 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