let p be Point of (TOP-REAL 2); :: thesis:
let f be FinSequence of (TOP-REAL 2); :: thesis:
let n be Element of NAT ; :: thesis:
set p1 = f /. 1;
set q = f /. n;
assume A1: ( p <> f /. 1 & f is being_S-Seq & p in LSeg f,n ) ; :: thesis:
then A2: f is special by TOPREAL1:def 10;
A3: n <= n + 1 by NAT_1:11;

A4: now

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

now

per cases by A5;

suppose not n in dom f ; :: thesis:

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

end;

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

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

end;

hence contradiction ; :: thesis:

end;

A6: ( f is one-to-one & Seg (len f) = dom f ) by A1, FINSEQ_1:def 3, TOPREAL1:def 10;
then A7: ( 1 <= n & n <= len f & n + 1 <= len f ) by A4, FINSEQ_1:3;

now

per cases ;

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

then n + 1 = n by A4, A6, PARTFUN2:17;
hence contradiction ; :: thesis:

end;

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

then 1 < n by A1, A7, XXREAL_0:1;
then A9: 1 + 1 <= n by NAT_1:13;

now

per cases by A9, XXREAL_0:1;

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

now

per cases ) `1 = p `1 or (f /. 1) `2 = p `2 ) by A2, A7, A8, A10, TOPREAL1:def 7;

suppose A11: (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, A8, A10, A11, Th16; :: thesis:

end;

suppose A12: (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, A8, A10, A12, Th15; :: 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 A13: 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 A1, A4, A8, A13, Th17; :: thesis:

end;

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

now

per cases by A7, XXREAL_0:1;

suppose A15: n = 1 ; :: thesis:

now

per cases ) `1 = p `1 or (f /. 1) `2 = p `2 ) by A2, A7, A14, A15, TOPREAL1:def 7;

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

end;

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

end;

suppose 1 < n ; :: thesis:

then A18: 1 + 1 < n + 1 by XREAL_1:8;
take h = f | (n + 1); :: 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, A4, A14, A18, Th17, TOPREAL3:45; :: thesis:

end;

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

now

per cases by A7, XXREAL_0:1;

suppose A20: n = 1 ; :: thesis:

A21: len f >= 1 + 1 by A1, TOPREAL1:def 10;
set q1 = f /. (1 + 1);
A22: LSeg f,n = LSeg (f /. 1),(f /. (1 + 1)) by A20, A21, TOPREAL1:def 5;

now

per cases ) `1 = (f /. (1 + 1)) `1 or (f /. 1) `2 = (f /. (1 + 1)) `2 ) by A2, A21, TOPREAL1:def 7;

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

then ( (f /. 1) `1 <= p `1 & p `1 <= (f /. (1 + 1)) `1 ) by A1, A22, TOPREAL1:9;
then A24: (f /. 1) `1 = p `1 by A23, XXREAL_0:1;
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, A20, A24, Th13; :: thesis:

end;

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

then ( (f /. 1) `2 <= p `2 & p `2 <= (f /. (1 + 1)) `2 ) by A1, A22, TOPREAL1:10;
then A26: (f /. 1) `2 = p `2 by A25, XXREAL_0:1;
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, A20, A26, Th12; :: thesis:

end;

suppose A27: 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 A1, A4, A19, A27, Th14; :: thesis:

end;