let p be Point of (TOP-REAL 2); :: thesis:
let f be FinSequence of (TOP-REAL 2); :: thesis:
let n be Nat; :: thesis:
set p1 = f /. 1;
set q = f /. n;
assume that
A1: p <> f /. 1 and
A2: f is being_S-Seq and
A3: p in LSeg (f,n) ; :: thesis:
A4: f is special by A2;
A5: n <= n + 1 by NAT_1:11;

A6: now :: thesis:

assume A7: ( not n in dom f or not n + 1 in dom f ) ; :: thesis:

now :: thesis:

per cases by A7;

suppose not n in dom f ; :: thesis:

then ( not 1 <= n or not n <= len f ) by FINSEQ_3:25;
then ( not 1 <= n or not n + 1 <= len f ) by A5, XXREAL_0:2;
hence contradiction by A3, TOPREAL1:def 3; :: thesis:

end;

suppose not n + 1 in dom f ; :: thesis:

then ( not 1 <= n + 1 or not n + 1 <= len f ) by FINSEQ_3:25;
hence contradiction by A3, NAT_1:11, TOPREAL1:def 3; :: thesis:

end;

hence contradiction ; :: thesis:

end;

A8: f is one-to-one by A2;
A9: Seg (len f) = dom f by FINSEQ_1:def 3;
then A10: 1 <= n by A6, FINSEQ_1:1;
A11: n + 1 <= len f by A6, A9, FINSEQ_1:1;
A12: n <= len f by A6, A9, FINSEQ_1:1;

now :: thesis:

per cases ;

case ( f /. n = p & f /. (n + 1) = p ) ; :: thesis:

then n + 1 = n by A6, A8, PARTFUN2:10;
hence contradiction ; :: thesis:

end;

case A13: ( f /. n = p & f /. (n + 1) <> p ) ; :: thesis:

then 1 < n by A1, A10, XXREAL_0:1;
then A14: 1 + 1 <= n by NAT_1:13;

now :: thesis:

per cases by A14, XXREAL_0:1;

suppose A15: n = 1 + 1 ; :: thesis:

now :: thesis:

per cases ) `1 = p `1 or (f /. 1) `2 = p `2 ) by A4, A12, A13, A15;

suppose A16: (f /. 1) `1 = p `1 ; :: thesis:

take h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p*>; :: thesis:
thus ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by A1, A2, A13, A15, A16, Th15; :: thesis:

end;

suppose A17: (f /. 1) `2 = p `2 ; :: thesis:

take h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*>; :: thesis:
thus ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by A1, A2, A13, A15, A17, Th14; :: thesis:

end;

hence ex h being FinSequence of (TOP-REAL 2) st
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) ; :: thesis:

end;

suppose A18: n > 2 ; :: thesis:

take h = f | n; :: thesis:
thus ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by A2, A6, A13, A18, Th16; :: thesis:

end;

case A19: ( f /. n <> p & f /. (n + 1) = p ) ; :: thesis:

now :: thesis:

per cases by A10, XXREAL_0:1;

suppose A20: n = 1 ; :: thesis:

now :: thesis:

per cases ) `1 = p `1 or (f /. 1) `2 = p `2 ) by A4, A11, A19, A20;

suppose A21: (f /. 1) `1 = p `1 ; :: thesis:

end;

suppose A22: (f /. 1) `2 = p `2 ; :: thesis:

end;

suppose A23: 1 < n ; :: thesis:

take h = f | (n + 1); :: thesis:
1 + 1 < n + 1 by A23, XREAL_1:6;
hence ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by A2, A6, A19, Th16, TOPREAL3:38; :: thesis:

end;

case A24: ( f /. n <> p & f /. (n + 1) <> p ) ; :: thesis:

now :: thesis:

per cases by A10, XXREAL_0:1;

suppose A25: n = 1 ; :: thesis:

set q1 = f /. (1 + 1);
A26: len f >= 1 + 1 by A2;
then A27: LSeg (f,n) = LSeg ((f /. 1),(f /. (1 + 1))) by A25, TOPREAL1:def 3;

now :: thesis:

per cases ) `1 = (f /. (1 + 1)) `1 or (f /. 1) `2 = (f /. (1 + 1)) `2 ) by A4, A26;

suppose A28: (f /. 1) `1 = (f /. (1 + 1)) `1 ; :: thesis:

take h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p*>; :: thesis:
( (f /. 1) `1 <= p `1 & p `1 <= (f /. (1 + 1)) `1 ) by A3, A27, A28, TOPREAL1:3;
then (f /. 1) `1 = p `1 by A28, XXREAL_0:1;
hence ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by A1, A2, A3, A25, Th12; :: thesis:

end;

suppose A29: (f /. 1) `2 = (f /. (1 + 1)) `2 ; :: thesis:

take h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*>; :: thesis:
( (f /. 1) `2 <= p `2 & p `2 <= (f /. (1 + 1)) `2 ) by A3, A27, A29, TOPREAL1:4;
then (f /. 1) `2 = p `2 by A29, XXREAL_0:1;
hence ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by A1, A2, A3, A25, Th11; :: thesis:

end;

suppose A30: 1 < n ; :: thesis:

take h = (f | n) ^ <*p*>; :: thesis:
thus ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) ) by A2, A3, A6, A24, A30, Th13; :: thesis:

end;