let f be FinSequence of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & Index (p,f) < Index (q,f) holds

q in L~ (L_Cut (f,p))

let p, q be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) implies q in L~ (L_Cut (f,p)) )

assume that

A1: p in L~ f and

A2: q in L~ f and

A3: Index (p,f) < Index (q,f) ; :: thesis: q in L~ (L_Cut (f,p))

A4: Index (q,f) < len f by A2, Th8;

then A5: (Index (q,f)) - (Index (p,f)) <= (len f) - (Index (p,f)) by XREAL_1:9;

then A6: ((Index (q,f)) - (Index (p,f))) + 1 <= ((len f) - (Index (p,f))) + 1 by XREAL_1:6;

(Index (q,f)) - (Index (p,f)) <= (((len f) - (Index (p,f))) - 1) + 1 by A4, XREAL_1:9;

then A7: (Index (q,f)) -' (Index (p,f)) <= ((len f) - ((Index (p,f)) + 1)) + 1 by A3, XREAL_1:233;

set i1 = ((Index (q,f)) -' (Index (p,f))) + 1;

A8: 1 <= (Index (p,f)) + 1 by NAT_1:11;

A9: (Index (p,f)) + 1 <= Index (q,f) by A3, NAT_1:13;

then A10: ((Index (p,f)) + 1) - (Index (p,f)) <= (Index (q,f)) - (Index (p,f)) by XREAL_1:9;

then A11: 1 <= (Index (q,f)) -' (Index (p,f)) by XREAL_0:def 2;

then A12: 1 <= ((Index (q,f)) -' (Index (p,f))) + 1 by NAT_D:48;

1 + 1 <= ((Index (q,f)) -' (Index (p,f))) + 1 by A11, XREAL_1:6;

then A13: 1 < ((Index (q,f)) -' (Index (p,f))) + 1 by XXREAL_0:2;

then A14: len <*p*> < ((Index (q,f)) -' (Index (p,f))) + 1 by FINSEQ_1:40;

then A15: len <*p*> < (((Index (q,f)) -' (Index (p,f))) + 1) + 1 by NAT_1:13;

A16: (Index (p,f)) + 1 <= len f by A4, A9, XXREAL_0:2;

A17: 1 <= Index (q,f) by A2, Th8;

then 1 < len f by A4, XXREAL_0:2;

then len (mid (f,((Index (p,f)) + 1),(len f))) = ((len f) -' ((Index (p,f)) + 1)) + 1 by A8, A16, FINSEQ_6:118;

then A18: (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) = 1 + (((len f) -' ((Index (p,f)) + 1)) + 1) by FINSEQ_1:40

.= 1 + (((len f) - ((Index (p,f)) + 1)) + 1) by A4, A9, XREAL_1:233, XXREAL_0:2

.= ((len f) - (Index (p,f))) + 1 ;

then A19: ((Index (q,f)) -' (Index (p,f))) + 1 <= (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) by A3, A6, XREAL_1:233;

q in L~ (L_Cut (f,p))

let p, q be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & q in L~ f & Index (p,f) < Index (q,f) implies q in L~ (L_Cut (f,p)) )

assume that

A1: p in L~ f and

A2: q in L~ f and

A3: Index (p,f) < Index (q,f) ; :: thesis: q in L~ (L_Cut (f,p))

A4: Index (q,f) < len f by A2, Th8;

then A5: (Index (q,f)) - (Index (p,f)) <= (len f) - (Index (p,f)) by XREAL_1:9;

then A6: ((Index (q,f)) - (Index (p,f))) + 1 <= ((len f) - (Index (p,f))) + 1 by XREAL_1:6;

(Index (q,f)) - (Index (p,f)) <= (((len f) - (Index (p,f))) - 1) + 1 by A4, XREAL_1:9;

then A7: (Index (q,f)) -' (Index (p,f)) <= ((len f) - ((Index (p,f)) + 1)) + 1 by A3, XREAL_1:233;

set i1 = ((Index (q,f)) -' (Index (p,f))) + 1;

A8: 1 <= (Index (p,f)) + 1 by NAT_1:11;

A9: (Index (p,f)) + 1 <= Index (q,f) by A3, NAT_1:13;

then A10: ((Index (p,f)) + 1) - (Index (p,f)) <= (Index (q,f)) - (Index (p,f)) by XREAL_1:9;

then A11: 1 <= (Index (q,f)) -' (Index (p,f)) by XREAL_0:def 2;

then A12: 1 <= ((Index (q,f)) -' (Index (p,f))) + 1 by NAT_D:48;

1 + 1 <= ((Index (q,f)) -' (Index (p,f))) + 1 by A11, XREAL_1:6;

then A13: 1 < ((Index (q,f)) -' (Index (p,f))) + 1 by XXREAL_0:2;

then A14: len <*p*> < ((Index (q,f)) -' (Index (p,f))) + 1 by FINSEQ_1:40;

then A15: len <*p*> < (((Index (q,f)) -' (Index (p,f))) + 1) + 1 by NAT_1:13;

A16: (Index (p,f)) + 1 <= len f by A4, A9, XXREAL_0:2;

A17: 1 <= Index (q,f) by A2, Th8;

then 1 < len f by A4, XXREAL_0:2;

then len (mid (f,((Index (p,f)) + 1),(len f))) = ((len f) -' ((Index (p,f)) + 1)) + 1 by A8, A16, FINSEQ_6:118;

then A18: (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) = 1 + (((len f) -' ((Index (p,f)) + 1)) + 1) by FINSEQ_1:40

.= 1 + (((len f) - ((Index (p,f)) + 1)) + 1) by A4, A9, XREAL_1:233, XXREAL_0:2

.= ((len f) - (Index (p,f))) + 1 ;

then A19: ((Index (q,f)) -' (Index (p,f))) + 1 <= (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) by A3, A6, XREAL_1:233;

per cases
( p = f . ((Index (p,f)) + 1) or p <> f . ((Index (p,f)) + 1) )
;

end;

suppose A20:
p = f . ((Index (p,f)) + 1)
; :: thesis: q in L~ (L_Cut (f,p))

then A21:
len (L_Cut (f,p)) = (len f) - (Index (p,f))
by A1, Th26;

then len (L_Cut (f,p)) >= (Index (q,f)) -' (Index (p,f)) by A3, A5, XREAL_1:233;

then (L_Cut (f,p)) /. ((Index (q,f)) -' (Index (p,f))) = (L_Cut (f,p)) . ((Index (q,f)) -' (Index (p,f))) by A11, FINSEQ_4:15

.= (mid (f,((Index (p,f)) + 1),(len f))) . ((Index (q,f)) -' (Index (p,f))) by A20, Def3

.= f . ((((Index (p,f)) + 1) + ((Index (q,f)) -' (Index (p,f)))) - 1) by A11, A8, A16, A7, FINSEQ_6:122

.= f . ((((Index (p,f)) + 1) + ((Index (q,f)) - (Index (p,f)))) - 1) by A3, XREAL_1:233

.= f . (Index (q,f)) ;

then A22: (L_Cut (f,p)) /. ((Index (q,f)) -' (Index (p,f))) = f /. (Index (q,f)) by A2, A4, Th8, FINSEQ_4:15;

1 <= Index (q,f) by A2, Th8;

then A23: 1 <= (Index (q,f)) + 1 by NAT_D:48;

A24: q in LSeg (f,(Index (q,f))) by A2, Th9;

A25: Index (q,f) < len f by A2, Th8;

then A26: (Index (q,f)) + 1 <= len f by NAT_1:13;

then A27: ((Index (q,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f)) by XREAL_1:9;

then ((Index (q,f)) - (Index (p,f))) + 1 <= (len f) - (Index (p,f)) ;

then A28: ((Index (q,f)) -' (Index (p,f))) + 1 <= ((len f) - ((Index (p,f)) + 1)) + 1 by A3, XREAL_1:233;

((Index (q,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f)) by A26, XREAL_1:9;

then ((Index (q,f)) - (Index (p,f))) + 1 <= (len f) - (Index (p,f)) ;

then A29: ((Index (q,f)) -' (Index (p,f))) + 1 <= len (L_Cut (f,p)) by A10, A21, XREAL_0:def 2;

A30: (Index (q,f)) + 1 <= len f by A25, NAT_1:13;

((Index (q,f)) - (Index (p,f))) + 1 <= (len f) - (Index (p,f)) by A27;

then len (L_Cut (f,p)) >= ((Index (q,f)) -' (Index (p,f))) + 1 by A3, A21, XREAL_1:233;

then (L_Cut (f,p)) /. (((Index (q,f)) -' (Index (p,f))) + 1) = (L_Cut (f,p)) . (((Index (q,f)) -' (Index (p,f))) + 1) by A13, FINSEQ_4:15

.= (mid (f,((Index (p,f)) + 1),(len f))) . (((Index (q,f)) -' (Index (p,f))) + 1) by A20, Def3

.= f . ((((Index (p,f)) + 1) + (((Index (q,f)) -' (Index (p,f))) + 1)) - 1) by A12, A8, A16, A28, FINSEQ_6:122

.= f . ((((Index (p,f)) + 1) + (((Index (q,f)) - (Index (p,f))) + 1)) - 1) by A3, XREAL_1:233

.= f /. ((Index (q,f)) + 1) by A23, A30, FINSEQ_4:15 ;

then q in LSeg (((L_Cut (f,p)) /. ((Index (q,f)) -' (Index (p,f)))),((L_Cut (f,p)) /. (((Index (q,f)) -' (Index (p,f))) + 1))) by A17, A22, A26, A24, TOPREAL1:def 3;

hence q in L~ (L_Cut (f,p)) by A11, A29, SPPOL_2:15; :: thesis: verum

end;then len (L_Cut (f,p)) >= (Index (q,f)) -' (Index (p,f)) by A3, A5, XREAL_1:233;

then (L_Cut (f,p)) /. ((Index (q,f)) -' (Index (p,f))) = (L_Cut (f,p)) . ((Index (q,f)) -' (Index (p,f))) by A11, FINSEQ_4:15

.= (mid (f,((Index (p,f)) + 1),(len f))) . ((Index (q,f)) -' (Index (p,f))) by A20, Def3

.= f . ((((Index (p,f)) + 1) + ((Index (q,f)) -' (Index (p,f)))) - 1) by A11, A8, A16, A7, FINSEQ_6:122

.= f . ((((Index (p,f)) + 1) + ((Index (q,f)) - (Index (p,f)))) - 1) by A3, XREAL_1:233

.= f . (Index (q,f)) ;

then A22: (L_Cut (f,p)) /. ((Index (q,f)) -' (Index (p,f))) = f /. (Index (q,f)) by A2, A4, Th8, FINSEQ_4:15;

1 <= Index (q,f) by A2, Th8;

then A23: 1 <= (Index (q,f)) + 1 by NAT_D:48;

A24: q in LSeg (f,(Index (q,f))) by A2, Th9;

A25: Index (q,f) < len f by A2, Th8;

then A26: (Index (q,f)) + 1 <= len f by NAT_1:13;

then A27: ((Index (q,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f)) by XREAL_1:9;

then ((Index (q,f)) - (Index (p,f))) + 1 <= (len f) - (Index (p,f)) ;

then A28: ((Index (q,f)) -' (Index (p,f))) + 1 <= ((len f) - ((Index (p,f)) + 1)) + 1 by A3, XREAL_1:233;

((Index (q,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f)) by A26, XREAL_1:9;

then ((Index (q,f)) - (Index (p,f))) + 1 <= (len f) - (Index (p,f)) ;

then A29: ((Index (q,f)) -' (Index (p,f))) + 1 <= len (L_Cut (f,p)) by A10, A21, XREAL_0:def 2;

A30: (Index (q,f)) + 1 <= len f by A25, NAT_1:13;

((Index (q,f)) - (Index (p,f))) + 1 <= (len f) - (Index (p,f)) by A27;

then len (L_Cut (f,p)) >= ((Index (q,f)) -' (Index (p,f))) + 1 by A3, A21, XREAL_1:233;

then (L_Cut (f,p)) /. (((Index (q,f)) -' (Index (p,f))) + 1) = (L_Cut (f,p)) . (((Index (q,f)) -' (Index (p,f))) + 1) by A13, FINSEQ_4:15

.= (mid (f,((Index (p,f)) + 1),(len f))) . (((Index (q,f)) -' (Index (p,f))) + 1) by A20, Def3

.= f . ((((Index (p,f)) + 1) + (((Index (q,f)) -' (Index (p,f))) + 1)) - 1) by A12, A8, A16, A28, FINSEQ_6:122

.= f . ((((Index (p,f)) + 1) + (((Index (q,f)) - (Index (p,f))) + 1)) - 1) by A3, XREAL_1:233

.= f /. ((Index (q,f)) + 1) by A23, A30, FINSEQ_4:15 ;

then q in LSeg (((L_Cut (f,p)) /. ((Index (q,f)) -' (Index (p,f)))),((L_Cut (f,p)) /. (((Index (q,f)) -' (Index (p,f))) + 1))) by A17, A22, A26, A24, TOPREAL1:def 3;

hence q in L~ (L_Cut (f,p)) by A11, A29, SPPOL_2:15; :: thesis: verum

suppose A31:
p <> f . ((Index (p,f)) + 1)
; :: thesis: q in L~ (L_Cut (f,p))

A32:
len (L_Cut (f,p)) = ((len f) - (Index (p,f))) + 1
by A1, A31, Th26;

then len (L_Cut (f,p)) >= ((Index (q,f)) -' (Index (p,f))) + 1 by A3, A6, XREAL_1:233;

then (L_Cut (f,p)) /. (((Index (q,f)) -' (Index (p,f))) + 1) = (L_Cut (f,p)) . (((Index (q,f)) -' (Index (p,f))) + 1) by FINSEQ_4:15, NAT_1:11

.= (<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))) . (((Index (q,f)) -' (Index (p,f))) + 1) by A31, Def3

.= (mid (f,((Index (p,f)) + 1),(len f))) . ((((Index (q,f)) -' (Index (p,f))) + 1) - (len <*p*>)) by A14, A19, FINSEQ_6:108

.= (mid (f,((Index (p,f)) + 1),(len f))) . ((((Index (q,f)) -' (Index (p,f))) + 1) - 1) by FINSEQ_1:40

.= f . ((((Index (p,f)) + 1) + ((Index (q,f)) -' (Index (p,f)))) - 1) by A11, A8, A16, A7, FINSEQ_6:122

.= f . ((((Index (p,f)) + 1) + ((Index (q,f)) - (Index (p,f)))) - 1) by A3, XREAL_1:233

.= f . (Index (q,f)) ;

then A33: (L_Cut (f,p)) /. (((Index (q,f)) -' (Index (p,f))) + 1) = f /. (Index (q,f)) by A2, A4, Th8, FINSEQ_4:15;

A34: Index (q,f) < len f by A2, Th8;

then A35: (Index (q,f)) + 1 <= len f by NAT_1:13;

then A36: ((Index (q,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f)) by XREAL_1:9;

then ((Index (q,f)) - (Index (p,f))) + 1 <= (len f) - (Index (p,f)) ;

then A37: ((Index (q,f)) -' (Index (p,f))) + 1 <= ((len f) - ((Index (p,f)) + 1)) + 1 by A3, XREAL_1:233;

((Index (q,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f)) by A35, XREAL_1:9;

then ((Index (q,f)) - (Index (p,f))) + 1 <= (len f) - (Index (p,f)) ;

then ((Index (q,f)) -' (Index (p,f))) + 1 <= (len f) - (Index (p,f)) by A10, XREAL_0:def 2;

then A38: (((Index (q,f)) -' (Index (p,f))) + 1) + 1 <= len (L_Cut (f,p)) by A32, XREAL_1:6;

1 <= Index (q,f) by A2, Th8;

then A39: 1 <= (Index (q,f)) + 1 by NAT_D:48;

A40: q in LSeg (f,(Index (q,f))) by A2, Th9;

A41: (Index (q,f)) + 1 <= len f by A34, NAT_1:13;

A42: (((Index (q,f)) - (Index (p,f))) + 1) + 1 <= ((len f) - (Index (p,f))) + 1 by A36, XREAL_1:6;

then A43: (((Index (q,f)) -' (Index (p,f))) + 1) + 1 <= (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) by A3, A18, XREAL_1:233;

len (L_Cut (f,p)) >= (((Index (q,f)) -' (Index (p,f))) + 1) + 1 by A3, A32, A42, XREAL_1:233;

then (L_Cut (f,p)) /. ((((Index (q,f)) -' (Index (p,f))) + 1) + 1) = (L_Cut (f,p)) . ((((Index (q,f)) -' (Index (p,f))) + 1) + 1) by FINSEQ_4:15, NAT_1:11

.= (<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))) . ((((Index (q,f)) -' (Index (p,f))) + 1) + 1) by A31, Def3

.= (mid (f,((Index (p,f)) + 1),(len f))) . (((((Index (q,f)) -' (Index (p,f))) + 1) + 1) - (len <*p*>)) by A15, A43, FINSEQ_6:108

.= (mid (f,((Index (p,f)) + 1),(len f))) . (((((Index (q,f)) -' (Index (p,f))) + 1) + 1) - 1) by FINSEQ_1:40

.= f . ((((Index (p,f)) + 1) + (((Index (q,f)) -' (Index (p,f))) + 1)) - 1) by A12, A8, A16, A37, FINSEQ_6:122

.= f . ((((Index (p,f)) + 1) + (((Index (q,f)) - (Index (p,f))) + 1)) - 1) by A3, XREAL_1:233

.= f /. ((Index (q,f)) + 1) by A39, A41, FINSEQ_4:15 ;

then q in LSeg (((L_Cut (f,p)) /. (((Index (q,f)) -' (Index (p,f))) + 1)),((L_Cut (f,p)) /. ((((Index (q,f)) -' (Index (p,f))) + 1) + 1))) by A17, A33, A35, A40, TOPREAL1:def 3;

hence q in L~ (L_Cut (f,p)) by A38, NAT_1:11, SPPOL_2:15; :: thesis: verum

end;then len (L_Cut (f,p)) >= ((Index (q,f)) -' (Index (p,f))) + 1 by A3, A6, XREAL_1:233;

then (L_Cut (f,p)) /. (((Index (q,f)) -' (Index (p,f))) + 1) = (L_Cut (f,p)) . (((Index (q,f)) -' (Index (p,f))) + 1) by FINSEQ_4:15, NAT_1:11

.= (<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))) . (((Index (q,f)) -' (Index (p,f))) + 1) by A31, Def3

.= (mid (f,((Index (p,f)) + 1),(len f))) . ((((Index (q,f)) -' (Index (p,f))) + 1) - (len <*p*>)) by A14, A19, FINSEQ_6:108

.= (mid (f,((Index (p,f)) + 1),(len f))) . ((((Index (q,f)) -' (Index (p,f))) + 1) - 1) by FINSEQ_1:40

.= f . ((((Index (p,f)) + 1) + ((Index (q,f)) -' (Index (p,f)))) - 1) by A11, A8, A16, A7, FINSEQ_6:122

.= f . ((((Index (p,f)) + 1) + ((Index (q,f)) - (Index (p,f)))) - 1) by A3, XREAL_1:233

.= f . (Index (q,f)) ;

then A33: (L_Cut (f,p)) /. (((Index (q,f)) -' (Index (p,f))) + 1) = f /. (Index (q,f)) by A2, A4, Th8, FINSEQ_4:15;

A34: Index (q,f) < len f by A2, Th8;

then A35: (Index (q,f)) + 1 <= len f by NAT_1:13;

then A36: ((Index (q,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f)) by XREAL_1:9;

then ((Index (q,f)) - (Index (p,f))) + 1 <= (len f) - (Index (p,f)) ;

then A37: ((Index (q,f)) -' (Index (p,f))) + 1 <= ((len f) - ((Index (p,f)) + 1)) + 1 by A3, XREAL_1:233;

((Index (q,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f)) by A35, XREAL_1:9;

then ((Index (q,f)) - (Index (p,f))) + 1 <= (len f) - (Index (p,f)) ;

then ((Index (q,f)) -' (Index (p,f))) + 1 <= (len f) - (Index (p,f)) by A10, XREAL_0:def 2;

then A38: (((Index (q,f)) -' (Index (p,f))) + 1) + 1 <= len (L_Cut (f,p)) by A32, XREAL_1:6;

1 <= Index (q,f) by A2, Th8;

then A39: 1 <= (Index (q,f)) + 1 by NAT_D:48;

A40: q in LSeg (f,(Index (q,f))) by A2, Th9;

A41: (Index (q,f)) + 1 <= len f by A34, NAT_1:13;

A42: (((Index (q,f)) - (Index (p,f))) + 1) + 1 <= ((len f) - (Index (p,f))) + 1 by A36, XREAL_1:6;

then A43: (((Index (q,f)) -' (Index (p,f))) + 1) + 1 <= (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) by A3, A18, XREAL_1:233;

len (L_Cut (f,p)) >= (((Index (q,f)) -' (Index (p,f))) + 1) + 1 by A3, A32, A42, XREAL_1:233;

then (L_Cut (f,p)) /. ((((Index (q,f)) -' (Index (p,f))) + 1) + 1) = (L_Cut (f,p)) . ((((Index (q,f)) -' (Index (p,f))) + 1) + 1) by FINSEQ_4:15, NAT_1:11

.= (<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))) . ((((Index (q,f)) -' (Index (p,f))) + 1) + 1) by A31, Def3

.= (mid (f,((Index (p,f)) + 1),(len f))) . (((((Index (q,f)) -' (Index (p,f))) + 1) + 1) - (len <*p*>)) by A15, A43, FINSEQ_6:108

.= (mid (f,((Index (p,f)) + 1),(len f))) . (((((Index (q,f)) -' (Index (p,f))) + 1) + 1) - 1) by FINSEQ_1:40

.= f . ((((Index (p,f)) + 1) + (((Index (q,f)) -' (Index (p,f))) + 1)) - 1) by A12, A8, A16, A37, FINSEQ_6:122

.= f . ((((Index (p,f)) + 1) + (((Index (q,f)) - (Index (p,f))) + 1)) - 1) by A3, XREAL_1:233

.= f /. ((Index (q,f)) + 1) by A39, A41, FINSEQ_4:15 ;

then q in LSeg (((L_Cut (f,p)) /. (((Index (q,f)) -' (Index (p,f))) + 1)),((L_Cut (f,p)) /. ((((Index (q,f)) -' (Index (p,f))) + 1) + 1))) by A17, A33, A35, A40, TOPREAL1:def 3;

hence q in L~ (L_Cut (f,p)) by A38, NAT_1:11, SPPOL_2:15; :: thesis: verum