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;

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

end;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;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

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

hence
rng ((m,n) -cut p) c= rng p
by A1; :: thesis: verumassume
( 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;then (m,n) -cut p = {} by Def1;

then rng ((m,n) -cut p) = {} ;

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