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 ;
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 ;
0 + 1 <= z by ;
then consider i being Nat such that
0 <= i and
A9: i < len ((m,n) -cut p) and
A10: z = i + 1 by ;
m + i < (len ((m,n) -cut p)) + m by ;
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 ;
1 <= m + i by ;
then A12: m + i in dom p by ;
((m,n) -cut p) . z = p . (m + i) by A2, A4, A5, A9, A10, Lm2;
hence x in rng p by ; :: 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