let f be FinSequence of (); :: thesis: for p, q being Point of () 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 (); :: 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 ;
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 ;
then A7: (Index (q,f)) -' (Index (p,f)) <= ((len f) - ((Index (p,f)) + 1)) + 1 by ;
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 ;
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 ;
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 ;
A17: 1 <= Index (q,f) by ;
then 1 < len f by ;
then len (mid (f,((Index (p,f)) + 1),(len f))) = ((len f) -' ((Index (p,f)) + 1)) + 1 by ;
then A18: () + (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
.= ((len f) - (Index (p,f))) + 1 ;
then A19: ((Index (q,f)) -' (Index (p,f))) + 1 <= () + (len (mid (f,((Index (p,f)) + 1),(len f)))) by ;
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 ;
then len (L_Cut (f,p)) >= (Index (q,f)) -' (Index (p,f)) by ;
then (L_Cut (f,p)) /. ((Index (q,f)) -' (Index (p,f))) = (L_Cut (f,p)) . ((Index (q,f)) -' (Index (p,f))) by
.= (mid (f,((Index (p,f)) + 1),(len f))) . ((Index (q,f)) -' (Index (p,f))) by
.= f . ((((Index (p,f)) + 1) + ((Index (q,f)) -' (Index (p,f)))) - 1) by
.= f . ((((Index (p,f)) + 1) + ((Index (q,f)) - (Index (p,f)))) - 1) by
.= f . (Index (q,f)) ;
then A22: (L_Cut (f,p)) /. ((Index (q,f)) -' (Index (p,f))) = f /. (Index (q,f)) by ;
1 <= Index (q,f) by ;
then A23: 1 <= (Index (q,f)) + 1 by NAT_D:48;
A24: q in LSeg (f,(Index (q,f))) by ;
A25: Index (q,f) < len f by ;
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 ;
((Index (q,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f)) by ;
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 ;
A30: (Index (q,f)) + 1 <= len f by ;
((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 ;
then (L_Cut (f,p)) /. (((Index (q,f)) -' (Index (p,f))) + 1) = (L_Cut (f,p)) . (((Index (q,f)) -' (Index (p,f))) + 1) by
.= (mid (f,((Index (p,f)) + 1),(len f))) . (((Index (q,f)) -' (Index (p,f))) + 1) by
.= f . ((((Index (p,f)) + 1) + (((Index (q,f)) -' (Index (p,f))) + 1)) - 1) by
.= f . ((((Index (p,f)) + 1) + (((Index (q,f)) - (Index (p,f))) + 1)) - 1) by
.= f /. ((Index (q,f)) + 1) by ;
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 ;
hence q in L~ (L_Cut (f,p)) by ; :: 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 ;
then len (L_Cut (f,p)) >= ((Index (q,f)) -' (Index (p,f))) + 1 by ;
then (L_Cut (f,p)) /. (((Index (q,f)) -' (Index (p,f))) + 1) = (L_Cut (f,p)) . (((Index (q,f)) -' (Index (p,f))) + 1) by
.= (<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))) . (((Index (q,f)) -' (Index (p,f))) + 1) by
.= (mid (f,((Index (p,f)) + 1),(len f))) . ((((Index (q,f)) -' (Index (p,f))) + 1) - ()) by
.= (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
.= f . ((((Index (p,f)) + 1) + ((Index (q,f)) - (Index (p,f)))) - 1) by
.= f . (Index (q,f)) ;
then A33: (L_Cut (f,p)) /. (((Index (q,f)) -' (Index (p,f))) + 1) = f /. (Index (q,f)) by ;
A34: Index (q,f) < len f by ;
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 ;
((Index (q,f)) + 1) - (Index (p,f)) <= (len f) - (Index (p,f)) by ;
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 ;
then A38: (((Index (q,f)) -' (Index (p,f))) + 1) + 1 <= len (L_Cut (f,p)) by ;
1 <= Index (q,f) by ;
then A39: 1 <= (Index (q,f)) + 1 by NAT_D:48;
A40: q in LSeg (f,(Index (q,f))) by ;
A41: (Index (q,f)) + 1 <= len f by ;
A42: (((Index (q,f)) - (Index (p,f))) + 1) + 1 <= ((len f) - (Index (p,f))) + 1 by ;
then A43: (((Index (q,f)) -' (Index (p,f))) + 1) + 1 <= () + (len (mid (f,((Index (p,f)) + 1),(len f)))) by ;
len (L_Cut (f,p)) >= (((Index (q,f)) -' (Index (p,f))) + 1) + 1 by ;
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
.= (<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))) . ((((Index (q,f)) -' (Index (p,f))) + 1) + 1) by
.= (mid (f,((Index (p,f)) + 1),(len f))) . (((((Index (q,f)) -' (Index (p,f))) + 1) + 1) - ()) by
.= (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
.= f . ((((Index (p,f)) + 1) + (((Index (q,f)) - (Index (p,f))) + 1)) - 1) by
.= f /. ((Index (q,f)) + 1) by ;
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 ;
hence q in L~ (L_Cut (f,p)) by ; :: thesis: verum
end;
end;