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

A1: now :: thesis: ( 1 <= m & m <= n & n <= len p implies rng ((m,n) -cut p) c= rng p )

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 object ; :: 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 object such that
A6: z in dom ((m,n) -cut p) and
A7: x = ((m,n) -cut p) . z by FUNCT_1:def 3;
reconsider z = z as Element of NAT by A6;
A8: z <= len ((m,n) -cut p) by A6, FINSEQ_3:25;
0 + 1 <= z by A6, FINSEQ_3:25;
then consider i being 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:6;
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:25;
((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 3; :: thesis: verum

end;

end;

now :: thesis: ( ( not 1 <= m or not m <= n or not n <= len p ) implies rng ((m,n) -cut p) c= rng p )

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 ; :: thesis: verum

end;

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