let m, n be Nat; :: thesis: 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); :: thesis: (m,n) -cut f is special
set h = (m,n) -cut f;
let i be Nat; :: according to TOPREAL1:def 5 :: thesis: ( 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) ; :: thesis: ( (((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 ( not 1 <= m or not m <= n or not n <= len f ) ; :: thesis: ( (((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 (m,n) -cut f = {} by FINSEQ_6:def 4;
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 A2; :: thesis: verum

end;

suppose A3: ( 1 <= m & m <= n & n <= len f ) ; :: thesis: ( (((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; :: thesis: verum

end;

end;