let m, n be Nat; for f being non empty special FinSequence of (TOP-REAL 2) holds (m,n) -cut f is special
let f be non empty special FinSequence of (TOP-REAL 2); (m,n) -cut f is special
set h = (m,n) -cut f;
let i be Nat; TOPREAL1:def 5 ( not 1 <= i or not i + 1 <= len ((m,n) -cut f) or (((m,n) -cut f) /. i) `1 = (((m,n) -cut f) /. (i + 1)) `1 or (((m,n) -cut f) /. i) `2 = (((m,n) -cut f) /. (i + 1)) `2 )
assume that
A1:
1 <= i
and
A2:
i + 1 <= len ((m,n) -cut f)
; ( (((m,n) -cut f) /. i) `1 = (((m,n) -cut f) /. (i + 1)) `1 or (((m,n) -cut f) /. i) `2 = (((m,n) -cut f) /. (i + 1)) `2 )
per cases
( not 1 <= m or not m <= n or not n <= len f or ( 1 <= m & m <= n & n <= len f ) )
;
suppose A3:
( 1
<= m &
m <= n &
n <= len f )
;
( (((m,n) -cut f) /. i) `1 = (((m,n) -cut f) /. (i + 1)) `1 or (((m,n) -cut f) /. i) `2 = (((m,n) -cut f) /. (i + 1)) `2 )then A4:
1
+ 1
<= i + m
by A1, XREAL_1:7;
then A5:
1
<= i + m
by XXREAL_0:2;
A6:
(i -' 1) + m = (i + m) -' 1
by A1, NAT_D:38;
then A7:
1
<= (i -' 1) + m
by A4, NAT_D:55;
A8:
((i -' 1) + m) + 1 =
((i + m) -' 1) + 1
by A1, NAT_D:38
.=
i + m
by A4, XREAL_1:235, XXREAL_0:2
;
A9:
i < len ((m,n) -cut f)
by A2, NAT_1:13;
(len ((m,n) -cut f)) + m = n + 1
by A3, FINSEQ_6:def 4;
then
i + m < n + 1
by A9, XREAL_1:6;
then
i + m <= n
by NAT_1:13;
then A10:
i + m <= len f
by A3, XXREAL_0:2;
then A11:
(i -' 1) + m <= len f
by A6, NAT_D:44;
i -' 1
<= i
by NAT_D:44;
then A12:
i -' 1
< len ((m,n) -cut f)
by A9, XXREAL_0:2;
A13:
((m,n) -cut f) /. (i + 1) =
((m,n) -cut f) . (i + 1)
by A2, FINSEQ_4:15, NAT_1:11
.=
f . (i + m)
by A3, A9, FINSEQ_6:def 4
.=
f /. (i + m)
by A5, A10, FINSEQ_4:15
;
(i -' 1) + 1
= i
by A1, XREAL_1:235;
then ((m,n) -cut f) /. i =
((m,n) -cut f) . ((i -' 1) + 1)
by A1, A9, FINSEQ_4:15
.=
f . ((i -' 1) + m)
by A3, A12, FINSEQ_6:def 4
.=
f /. ((i -' 1) + m)
by A6, A4, A11, FINSEQ_4:15, NAT_D:55
;
hence
(
(((m,n) -cut f) /. i) `1 = (((m,n) -cut f) /. (i + 1)) `1 or
(((m,n) -cut f) /. i) `2 = (((m,n) -cut f) /. (i + 1)) `2 )
by A7, A10, A13, A8, TOPREAL1:def 5;
verum end;