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;
per cases ( p = f . ((Index (p,f)) + 1) or p <> f . ((Index (p,f)) + 1) ) ;
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;
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;
end;