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:27;
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))));
A6: (L~ g) /\ (L~ f) is closed ;
L~ g is_an_arc_of g /. 1,g /. (len g) by TOPREAL1:31;
then A7: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in (L~ g) /\ (L~ f) by A3, JORDAN5C:def 2;
then A8: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in L~ g by XBOOLE_0:def 4;
then A9: 1 <= Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) by JORDAN3:41;
A10: 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 A8, JORDAN3:42;
A11: Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) < len g by A8, JORDAN3:41;
then A12: (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 A13: n in dom (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) and
A14: ( 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
A15: 1 <= n by A13, FINSEQ_3:27;
then A16: ((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 A17: (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n in LeftComp f by A14;
A18: 1 <= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 by NAT_1:11;
then A19: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 in dom g by A12, FINSEQ_3:27;
A20: LeftComp f misses RightComp f by SPRECT_1:96;
A21: L~ f misses LeftComp f by Th43;
A22: len g in dom g by FINSEQ_5:6;
A23: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in L~ f by A7, XBOOLE_0:def 4;

now

assume A24: 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 4;
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 A24, FINSEQ_5:16;
hence contradiction by A21, A23, A17, XBOOLE_0:3; :: thesis: verum

end;

suppose A25: 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 4;
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 A22, A13, A12, A19, A24, SPRECT_2:7
.= 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 A19, A25, PARTFUN1:def 8 ;
hence contradiction by A21, A23, A17, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

then A26: n > 1 by A15, XXREAL_0:1;
then A27: 1 + 1 < (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A9, XREAL_1:10;
then A28: 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));
A29: len <*(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))*> = 1 by FINSEQ_1:56;
A30: n <= len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) by A13, FINSEQ_3:27;
then A31: 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:8;
A32: n = (n -' 1) + 1 by A15, XREAL_1:237;
then A33: 1 <= n -' 1 by A26, NAT_1:13;
A34: 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 A12, A18, JORDAN4:20
.= (len g) -' (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) by A8, JORDAN3:41, NAT_2:9 ;
then A35: ((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 A11, XREAL_1:237;

now

A36: (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 A16, A33, XREAL_1:8;
assume A37: 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 A38: 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 4;
then A39: 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 A29, FINSEQ_1:35;
then A40: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 <= len g by A35, A31, NAT_D:53;
A41: (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 A39, 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 A30, NAT_D:42;
then A42: n -' 1 in dom (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by A33, FINSEQ_3:27;
(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 A30, A32, A29, A33, A38, A41, NAT_D:42, SEQ_4:153;
then A43: (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 A22, A12, A19, A42, SPRECT_2:7
.= g /. ((n + (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) -' 1) by A32 ;
then A44: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 <> len g by A2, A17, A20, XBOOLE_0:3;
then A45: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 < len g by A40, 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, A28, A40, A44, JORDAN3:39;
A46: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 in dom g by A28, A40, FINSEQ_3:27;
then A47: m /. (len m) in RightComp f by A2, A22, SPRECT_2:13;
m /. 1 in LeftComp f by A22, A17, A43, A46, SPRECT_2:12;
then L~ f meets L~ m by A47, Th50;
then consider q being set such that
A48: q in L~ f and
A49: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A49;
consider i being Element of NAT such that
A50: 1 <= i and
A51: i + 1 <= len m and
A52: q in LSeg (m,i) by A49, SPPOL_2:13;
A53: len m = ((len g) -' (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) + 1 by A28, A40, JORDAN4:20;
then i <= (len g) -' (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) by A51, XREAL_1:8;
then A54: i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) <= len g by A40, NAT_D:54;
i < len m by A51, NAT_1:13;
then A55: LSeg (m,i) = LSeg (g,((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1)) by A28, A50, A53, A45, JORDAN4:31;
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 A56: ((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1) + 1 <= len g by A50, A54, XREAL_1:237, 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 A50, 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 A57: (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 A36, XXREAL_0:2;
A58: 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 A19, A37, PARTFUN1:def 8;

A59: now

assume Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = q ; :: thesis: contradiction
then A60: 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 A10, A52, A55, XBOOLE_0:def 4;
then A61: 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 A57, XXREAL_0:1;

suppose A62: (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 A56;
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 A9, TOPREAL1:def 8;
hence contradiction by A58, A60, A62, 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 A61, TOPREAL1:def 9; :: thesis: verum

end;

end;

end;

1 <= (i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1 by A18, A57, 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, A10, A12, A9, A48, A52, A55, A56, A59, 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 A57, XXREAL_0:2;
hence contradiction by XREAL_1:31; :: thesis: verum

end;

then A63: 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 4;
then A64: (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 A11, A34, XREAL_1:237;
then A65: 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 A31, FINSEQ_6:123;
A66: 1 <= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A27, 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 A27, XREAL_1:237, XXREAL_0:2;
then ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 < len g by A31, A64, NAT_1:13;
then A67: (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, A65, JORDAN4:18;
A68: (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 A22, A13, A12, A19, A63, SPRECT_2:7
.= 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 A69: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n <> len g by A2, A17, A20, 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, A31, A64, A66, JORDAN3:39;
(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n in dom g by A31, A64, A66, FINSEQ_3:27;
then m /. 1 in LeftComp f by A22, A17, A68, SPRECT_2:12;
then L~ f meets L~ m by A67, Th50;
then consider q being set such that
A70: q in L~ f and
A71: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A71;
consider i being Element of NAT such that
A72: 1 <= i and
A73: i + 1 <= len m and
A74: q in LSeg (m,i) by A71, SPPOL_2:13;
set j = (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1;
A75: (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 A72, NAT_D:38;
then A76: (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, A31, A64, A66, FINSEQ_6:124;
then A77: i < ((len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) + 1 by A73, NAT_1:13;
then i -' 1 < (len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) by A72, 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 A78: ((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1) + 1 <= len g by A75, NAT_1:13;
(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n < len g by A31, A64, A69, XXREAL_0:1;
then A79: LSeg (m,i) = LSeg (g,((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1)) by A66, A72, A77, JORDAN4:31;
(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 A26, XREAL_1:8;
then A80: (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 A76, XXREAL_0:2;

A81: 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 A10, A74, A79, 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 A80, TOPREAL1:def 9; :: thesis: verum

end;

1 <= (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 by A66, A76, 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, A10, A12, A9, A70, A74, A79, A81, A78, 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 A80, XXREAL_0:2;
hence contradiction by XREAL_1:31; :: thesis: verum