let f be rectangular special_circular_sequence; :: thesis: for g being S-Sequence_in_R2 st g /. 1 in LeftComp f & g /. (len g) in RightComp f holds
L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) is_in_the_area_of f
let g be S-Sequence_in_R2; :: thesis: ( g /. 1 in LeftComp f & g /. (len g) in RightComp f implies L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) is_in_the_area_of f )
assume that
A1: g /. 1 in LeftComp f and
A2: g /. (len g) in RightComp f ; :: thesis: L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) is_in_the_area_of f
A3: L~ g meets L~ f by A1, A2, Th50;
1 in dom g by FINSEQ_5:6;
then A4: len g >= 1 by FINSEQ_3:25;
set lp = Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f));
set ilp = Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g);
set h = L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))));
L~ g is_an_arc_of g /. 1,g /. (len g) by TOPREAL1:25;
then A6: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in (L~ g) /\ (L~ f) by A3, JORDAN5C:def 2;
then A7: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in L~ g by XBOOLE_0:def 4;
then A8: 1 <= Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) by JORDAN3:8;
A9: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) by A7, JORDAN3:9;
A10: Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) < len g by A7, JORDAN3:8;
then A11: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 <= len g by NAT_1:13;
given n being Element of NAT such that A12: n in dom (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) and
A13: ( W-bound (L~ f) > ((L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n) `1 or ((L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n) `1 > E-bound (L~ f) or S-bound (L~ f) > ((L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n) `2 or ((L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n) `2 > N-bound (L~ f) ) ; :: according to SPRECT_2:def 1 :: thesis: contradiction
A14: 1 <= n by A12, FINSEQ_3:25;
then A15: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 = (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + (n -' 1) by NAT_D:38;
LeftComp f = { p where p is Point of (TOP-REAL 2) : ( not W-bound (L~ f) <= p `1 or not p `1 <= E-bound (L~ f) or not S-bound (L~ f) <= p `2 or not p `2 <= N-bound (L~ f) ) } by Th54;
then A16: (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n in LeftComp f by A13;
A17: 1 <= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 by NAT_1:11;
then A18: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 in dom g by A11, FINSEQ_3:25;
A19: LeftComp f misses RightComp f by SPRECT_1:88;
A20: L~ f misses LeftComp f by Th43;
A21: len g in dom g by FINSEQ_5:6;
A22: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in L~ f by A6, XBOOLE_0:def 4;

now

assume A23: n = 1 ; :: thesis: contradiction

per cases ( Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> g . ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) or Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = g . ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) ) ;

suppose Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> g . ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) ; :: thesis: contradiction

then L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) = <*(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))*> ^ (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by JORDAN3:def 3;
then (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n = Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) by A23, FINSEQ_5:15;
hence contradiction by A20, A22, A16, XBOOLE_0:3; :: thesis: verum

end;

suppose A24: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = g . ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) ; :: thesis: contradiction

then L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) = mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g)) by JORDAN3:def 3;
then (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n = g /. ((1 + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1)) -' 1) by A21, A12, A11, A18, A23, SPRECT_2:3
.= g /. ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) by NAT_D:34
.= Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) by A18, A24, PARTFUN1:def 6 ;
hence contradiction by A20, A22, A16, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

then A25: n > 1 by A14, XXREAL_0:1;
then A26: 1 + 1 < (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A8, XREAL_1:8;
then A27: 1 <= ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 by NAT_D:49;
set m = mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n),(len g));
A28: len <*(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))*> = 1 by FINSEQ_1:39;
A29: n <= len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) by A12, FINSEQ_3:25;
then A30: n + (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) <= (len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))))) + (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) by XREAL_1:6;
A31: n = (n -' 1) + 1 by A14, XREAL_1:235;
then A32: 1 <= n -' 1 by A25, NAT_1:13;
A33: len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) = ((len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1)) + 1 by A11, A17, JORDAN4:8
.= (len g) -' (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) by A7, JORDAN3:8, NAT_2:7 ;
then A34: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + (len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))))) + 1 = (len g) + 1 by A10, XREAL_1:235;

now

A35: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 <= ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 by A15, A32, XREAL_1:6;
assume A36: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> g . ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) ; :: thesis: contradiction
then A37: L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) = <*(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))*> ^ (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by JORDAN3:def 3;
then A38: len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) = 1 + (len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g)))) by A28, FINSEQ_1:22;
then A39: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 <= len g by A34, A30, NAT_D:53;
A40: (len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))))) -' 1 = len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by A38, NAT_D:34;
then n -' 1 <= len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by A29, NAT_D:42;
then A41: n -' 1 in dom (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by A32, FINSEQ_3:25;
(L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n = (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) /. (n -' 1) by A29, A31, A28, A32, A37, A40, NAT_D:42, SEQ_4:136;
then A42: (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n = g /. (((n -' 1) + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1)) -' 1) by A21, A11, A18, A41, SPRECT_2:3
.= g /. ((n + (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) -' 1) by A31 ;
then A43: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 <> len g by A2, A16, A19, XBOOLE_0:3;
then A44: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 < len g by A39, XXREAL_0:1;
reconsider m = mid (g,(((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1),(len g)) as S-Sequence_in_R2 by A4, A27, A39, A43, JORDAN3:6;
A45: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 in dom g by A27, A39, FINSEQ_3:25;
then A46: m /. (len m) in RightComp f by A2, A21, SPRECT_2:9;
m /. 1 in LeftComp f by A21, A16, A42, A45, SPRECT_2:8;
then L~ f meets L~ m by A46, Th50;
then consider q being set such that
A47: q in L~ f and
A48: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A48;
consider i being Element of NAT such that
A49: 1 <= i and
A50: i + 1 <= len m and
A51: q in LSeg (m,i) by A48, SPPOL_2:13;
A52: len m = ((len g) -' (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) + 1 by A27, A39, JORDAN4:8;
then i <= (len g) -' (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) by A50, XREAL_1:6;
then A53: i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) <= len g by A39, NAT_D:54;
i < len m by A50, NAT_1:13;
then A54: LSeg (m,i) = LSeg (g,((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1)) by A27, A49, A52, A44, JORDAN4:19;
set j = (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1;
i <= i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) by NAT_1:11;
then A55: ((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1) + 1 <= len g by A49, A53, XREAL_1:235, XXREAL_0:2;
(i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 = (i -' 1) + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) by A49, NAT_D:38;
then (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 >= ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 by NAT_1:11;
then A56: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 <= (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 by A35, XXREAL_0:2;
A57: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) <> g /. ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1) by A18, A36, PARTFUN1:def 6;

A58: now

assume Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = q ; :: thesis: contradiction
then A59: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in (LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)))) /\ (LSeg (g,((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1))) by A9, A51, A54, XBOOLE_0:def 4;
then A60: LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) meets LSeg (g,((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1)) by XBOOLE_0:4;

per cases ( (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 = (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 or (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 < (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 ) by A56, XXREAL_0:1;

suppose A61: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 = (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 ; :: thesis: contradiction

then (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + (1 + 1) <= len g by A55;
then (LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)))) /\ (LSeg (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1))) = {(g /. ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1))} by A8, TOPREAL1:def 6;
hence contradiction by A57, A59, A61, TARSKI:def 1; :: thesis: verum

end;

suppose (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 < (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 ; :: thesis: contradiction

hence contradiction by A60, TOPREAL1:def 7; :: thesis: verum

end;

end;

end;

1 <= (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 by A17, A56, XXREAL_0:2;
then Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) >= (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 by A3, A9, A11, A8, A47, A51, A54, A55, A58, JORDAN5C:28;
then Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) >= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 by A56, XXREAL_0:2;
hence contradiction by XREAL_1:29; :: thesis: verum

end;

then A62: L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))) = mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g)) by JORDAN3:def 3;
then A63: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + (len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))))) = len g by A10, A33, XREAL_1:235;
then A64: mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n),(len g)) = g /^ (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) by A30, FINSEQ_6:117;
A65: 1 <= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A26, XXREAL_0:2;
(((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) + 1 = (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A26, XREAL_1:235, XXREAL_0:2;
then ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 < len g by A30, A63, NAT_1:13;
then A66: (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n),(len g))) /. (len (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n),(len g)))) in RightComp f by A2, A64, JORDAN4:6;
A67: (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n = g /. ((n + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1)) -' 1) by A21, A12, A11, A18, A62, SPRECT_2:3
.= g /. (((n + (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) + 1) -' 1)
.= g /. ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) by NAT_D:34 ;
then A68: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n <> len g by A2, A16, A19, XBOOLE_0:3;
then reconsider m = mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n),(len g)) as S-Sequence_in_R2 by A4, A30, A63, A65, JORDAN3:6;
(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n in dom g by A30, A63, A65, FINSEQ_3:25;
then m /. 1 in LeftComp f by A21, A16, A67, SPRECT_2:8;
then L~ f meets L~ m by A66, Th50;
then consider q being set such that
A69: q in L~ f and
A70: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A70;
consider i being Element of NAT such that
A71: 1 <= i and
A72: i + 1 <= len m and
A73: q in LSeg (m,i) by A70, SPPOL_2:13;
set j = (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1;
A74: (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 = (i -' 1) + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) by A71, NAT_D:38;
then A75: (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 >= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by NAT_1:11;
len m = ((len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) + 1 by A4, A30, A63, A65, FINSEQ_6:118;
then A76: i < ((len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) + 1 by A72, NAT_1:13;
then i -' 1 < (len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) by A71, NAT_D:54;
then (i -' 1) + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) < len g by NAT_D:53;
then A77: ((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1) + 1 <= len g by A74, NAT_1:13;
(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n < len g by A30, A63, A68, XXREAL_0:1;
then A78: LSeg (m,i) = LSeg (g,((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1)) by A65, A71, A76, JORDAN4:19;
(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 < (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A25, XREAL_1:6;
then A79: (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 > (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 by A75, XXREAL_0:2;

A80: now

assume Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = q ; :: thesis: contradiction
then Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in (LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)))) /\ (LSeg (g,((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1))) by A9, A73, A78, XBOOLE_0:def 4;
then LSeg (g,(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) meets LSeg (g,((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1)) by XBOOLE_0:4;
hence contradiction by A79, TOPREAL1:def 7; :: thesis: verum

end;

1 <= (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 by A65, A75, XXREAL_0:2;
then Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) >= (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 by A3, A9, A11, A8, A69, A73, A78, A80, A77, JORDAN5C:28;
then Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) >= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 by A79, XXREAL_0:2;
hence contradiction by XREAL_1:29; :: thesis: verum