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, Th33;
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 A5: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in (L~ g) /\ (L~ f) by A3, JORDAN5C:def 2;
then A6: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in L~ g by XBOOLE_0:def 4;
then A7: 1 <= Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) by JORDAN3:8;
A8: 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 A6, JORDAN3:9;
A9: Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g) < len g by A6, JORDAN3:8;
then A10: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 <= len g by NAT_1:13;
given n being Nat such that A11: n in dom (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) and
A12: ( 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
A13: 1 <= n by A11, FINSEQ_3:25;
then A14: ((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 Th37;
then A15: (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) /. n in LeftComp f by A12;
A16: 1 <= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 by NAT_1:11;
then A17: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1 in dom g by A10, FINSEQ_3:25;
A18: LeftComp f misses RightComp f by SPRECT_1:88;
A19: L~ f misses LeftComp f by Th26;
A20: len g in dom g by FINSEQ_5:6;
A21: Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) in L~ f by A5, XBOOLE_0:def 4;
now :: thesis: not n = 1
assume A22: 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 A22, FINSEQ_5:15;
hence contradiction by A19, A21, A15, XBOOLE_0:3; :: thesis: verum
end;
suppose A23: 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 A20, A11, A10, A17, A22, 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 A17, A23, PARTFUN1:def 6 ;
hence contradiction by A19, A21, A15, XBOOLE_0:3; :: thesis: verum
end;
end;
end;
then A24: n > 1 by A13, XXREAL_0:1;
then A25: 1 + 1 < (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A7, XREAL_1:8;
then A26: 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));
A27: len <*(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)))*> = 1 by FINSEQ_1:39;
A28: n <= len (L_Cut (g,(Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))))) by A11, FINSEQ_3:25;
then A29: 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;
A30: n = (n -' 1) + 1 by A13, XREAL_1:235;
then A31: 1 <= n -' 1 by A24, NAT_1:13;
A32: 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 A10, A16, JORDAN4:8
.= (len g) -' (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) by A6, JORDAN3:8, NAT_2:7 ;
then A33: ((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 A9, XREAL_1:235;
now :: thesis: not 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)
A34: (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 A14, A31, XREAL_1:6;
assume A35: 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 A36: 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 A37: 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 A27, FINSEQ_1:22;
then A38: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 <= len g by A33, A29, NAT_D:53;
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 A37, 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 A28, NAT_D:42;
then A40: n -' 1 in dom (mid (g,((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + 1),(len g))) by A31, 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 A28, A30, A27, A31, A36, A39, NAT_D:42, SEQ_4:136;
then A41: (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 A20, A10, A17, A40, SPRECT_2:3
.= g /. ((n + (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g))) -' 1) by A30 ;
then A42: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 <> len g by A2, A15, A18, XBOOLE_0:3;
then A43: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 < len g by A38, 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, A26, A38, A42, JORDAN3:6;
A44: ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1 in dom g by A26, A38, FINSEQ_3:25;
then A45: m /. (len m) in RightComp f by A2, A20, SPRECT_2:9;
m /. 1 in LeftComp f by A20, A15, A41, A44, SPRECT_2:8;
then L~ f meets L~ m by A45, Th33;
then consider q being object such that
A46: q in L~ f and
A47: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A47;
consider i being Nat such that
A48: 1 <= i and
A49: i + 1 <= len m and
A50: q in LSeg (m,i) by A47, SPPOL_2:13;
A51: len m = ((len g) -' (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) + 1 by A26, A38, JORDAN4:8;
then i <= (len g) -' (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) by A49, XREAL_1:6;
then A52: i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1) <= len g by A38, NAT_D:54;
i < len m by A49, NAT_1:13;
then A53: LSeg (m,i) = LSeg (g,((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1)) by A26, A48, A51, A43, 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 A54: ((i + (((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) -' 1)) -' 1) + 1 <= len g by A48, A52, 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 A48, 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 A55: (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 A34, XXREAL_0:2;
A56: 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 A17, A35, PARTFUN1:def 6;
A57: now :: thesis: not Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = q
assume Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = q ; :: thesis: contradiction
then A58: 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 A8, A50, A53, XBOOLE_0:def 4;
then A59: 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)) ;
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 A55, XXREAL_0:1;
suppose A60: (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 A54;
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 A7, TOPREAL1:def 6;
hence contradiction by A56, A58, A60, 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 A59, 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 A16, A55, 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, A8, A10, A7, A46, A50, A53, A54, A57, 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 A55, XXREAL_0:2;
hence contradiction by XREAL_1:29; :: thesis: verum
end;
then A61: 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 A62: (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 A9, A32, XREAL_1:235;
then A63: 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 A29, FINSEQ_6:117;
A64: 1 <= (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n by A25, 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 A25, 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 A29, A62, NAT_1:13;
then A65: (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, A63, JORDAN4:6;
A66: (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 A20, A11, A10, A17, A61, 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 A67: (Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n <> len g by A2, A15, A18, 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, A29, A62, A64, JORDAN3:6;
(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n in dom g by A29, A62, A64, FINSEQ_3:25;
then m /. 1 in LeftComp f by A20, A15, A66, SPRECT_2:8;
then L~ f meets L~ m by A65, Th33;
then consider q being object such that
A68: q in L~ f and
A69: q in L~ m by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A69;
consider i being Nat such that
A70: 1 <= i and
A71: i + 1 <= len m and
A72: q in LSeg (m,i) by A69, SPPOL_2:13;
set j = (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1;
A73: (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 A70, NAT_D:38;
then A74: (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, A29, A62, A64, FINSEQ_6:118;
then A75: i < ((len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) + 1 by A71, NAT_1:13;
then i -' 1 < (len g) -' ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n) by A70, 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 A76: ((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1) + 1 <= len g by A73, NAT_1:13;
(Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n < len g by A29, A62, A67, XXREAL_0:1;
then A77: LSeg (m,i) = LSeg (g,((i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1)) by A64, A70, A75, 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 A24, XREAL_1:6;
then A78: (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 A74, XXREAL_0:2;
A79: now :: thesis: not Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f)) = q
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 A8, A72, A77, 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)) ;
hence contradiction by A78, TOPREAL1:def 7; :: thesis: verum
end;
1 <= (i + ((Index ((Last_Point ((L~ g),(g /. 1),(g /. (len g)),(L~ f))),g)) + n)) -' 1 by A64, A74, 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, A8, A10, A7, A68, A72, A77, A79, A76, 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 A78, XXREAL_0:2;
hence contradiction by XREAL_1:29; :: thesis: verum