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 & p <> q & Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) 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 & p <> q & Index (p,f) = Index (q,f) & LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) implies q in L~ (L_Cut (f,p)) )
assume that
A1: p in L~ f and
A2: q in L~ f and
A3: p <> q and
A4: Index (p,f) = Index (q,f) and
A5: LE p,q,f /. (Index (p,f)),f /. ((Index (p,f)) + 1) ; :: thesis: q in L~ (L_Cut (f,p))
A6: (Index (q,f)) -' (Index (p,f)) = (Index (q,f)) - (Index (p,f)) by A4, XREAL_1:235
.= 0 by A4 ;
Index (q,f) < len f by A2, Th41;
then A7: (Index (q,f)) + 1 <= len f by NAT_1:13;

A8: now

q in LSeg ((f /. (Index (p,f))),(f /. ((Index (p,f)) + 1))) by A5, Def6;
then consider r being Real such that
A9: q = ((1 - r) * (f /. (Index (p,f)))) + (r * (f /. ((Index (p,f)) + 1))) and
A10: 0 <= r and
A11: r <= 1 ;
A12: p = 1 * p by EUCLID:33
.= (0. (TOP-REAL 2)) + (1 * p) by EUCLID:31
.= ((1 - 1) * (f /. (Index (p,f)))) + (1 * p) by EUCLID:33 ;
assume A13: p = f . ((Index (p,f)) + 1) ; :: thesis: contradiction
then p = f /. ((Index (p,f)) + 1) by A4, A7, FINSEQ_4:24, NAT_1:11;
then 1 <= r by A5, A9, A10, A12, Def6;
then r = 1 by A11, XXREAL_0:1;
hence contradiction by A3, A4, A7, A13, A9, A12, FINSEQ_4:24, NAT_1:11; :: thesis: verum

end;

then A14: len (L_Cut (f,p)) = ((len f) - (Index (p,f))) + 1 by A1, Th61;
1 <= Index (q,f) by A2, Th41;
then A15: 1 <= (Index (q,f)) + 1 by NAT_D:48;
1 < (0 + 1) + 1 ;
then A16: len <*p*> < (((Index (q,f)) -' (Index (p,f))) + 1) + 1 by A6, FINSEQ_1:57;
A17: Index (q,f) < len f by A2, Th41;
then A18: (Index (q,f)) + 1 <= len f by NAT_1:13;
then A19: ((Index (q,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f)) by XREAL_1:11;
then A20: (((Index (q,f)) - (Index (p,f))) + 1) + 1 <= ((len f) - (Index (p,f))) + 1 by XREAL_1:8;
((Index (q,f)) - (Index (p,f))) + 1 <= (len f) - (Index (p,f)) by A19;
then A21: ((Index (q,f)) -' (Index (p,f))) + 1 <= ((len f) - ((Index (p,f)) + 1)) + 1 by A4, XREAL_1:235;
A22: 1 <= (Index (p,f)) + 1 by NAT_1:11;
A23: Index (q,f) < len f by A2, Th41;
then (Index (q,f)) - (Index (p,f)) <= (len f) - (Index (p,f)) by XREAL_1:11;
then ((Index (q,f)) - (Index (p,f))) + 1 <= ((len f) - (Index (p,f))) + 1 by XREAL_1:8;
then A24: (L_Cut (f,p)) /. (((Index (q,f)) -' (Index (p,f))) + 1) = (L_Cut (f,p)) . (((Index (q,f)) -' (Index (p,f))) + 1) by A4, A6, A14, FINSEQ_4:24
.= (<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))) . (((Index (q,f)) -' (Index (p,f))) + 1) by A8, Def4
.= p by A6, FINSEQ_1:58 ;
set i1 = ((Index (q,f)) -' (Index (p,f))) + 1;
A25: (Index (q,f)) + 1 <= len f by A17, NAT_1:13;
((Index (q,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f)) by A18, XREAL_1:11;
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 A4, XREAL_0:def 2;
then A26: (((Index (q,f)) -' (Index (p,f))) + 1) + 1 <= len (L_Cut (f,p)) by A14, XREAL_1:8;
1 <= Index (q,f) by A2, Th41;
then 1 < len f by A23, XXREAL_0:2;
then len (mid (f,((Index (p,f)) + 1),(len f))) = ((len f) -' ((Index (p,f)) + 1)) + 1 by A4, A7, A22, FINSEQ_6:124;
then (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) = 1 + (((len f) -' ((Index (p,f)) + 1)) + 1) by FINSEQ_1:57
.= 1 + (((len f) - ((Index (p,f)) + 1)) + 1) by A4, A7, XREAL_1:235
.= ((len f) - (Index (p,f))) + 1 ;
then A27: (((Index (q,f)) -' (Index (p,f))) + 1) + 1 <= (len <*p*>) + (len (mid (f,((Index (p,f)) + 1),(len f)))) by A4, A20, XREAL_1:235;
(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 A4, A6, A14, A20, FINSEQ_4:24
.= (<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))) . ((((Index (q,f)) -' (Index (p,f))) + 1) + 1) by A8, Def4
.= (mid (f,((Index (p,f)) + 1),(len f))) . (((((Index (q,f)) -' (Index (p,f))) + 1) + 1) - (len <*p*>)) by A16, A27, FINSEQ_6:114
.= (mid (f,((Index (p,f)) + 1),(len f))) . (((((Index (q,f)) -' (Index (p,f))) + 1) + 1) - 1) by FINSEQ_1:57
.= f . ((((Index (p,f)) + 1) + (((Index (q,f)) - (Index (p,f))) + 1)) - 1) by A4, A7, A6, A22, A21, FINSEQ_6:128
.= f /. ((Index (q,f)) + 1) by A15, A25, FINSEQ_4:24 ;
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 A4, A5, A24, Th65;
hence q in L~ (L_Cut (f,p)) by A6, A26, SPPOL_2:15; :: thesis: verum