let p be Point of (TOP-REAL 2); :: thesis: for f being FinSequence of (TOP-REAL 2)

for n being Nat st p <> f /. 1 & f is being_S-Seq & p in LSeg (f,n) holds

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)) )

let f be FinSequence of (TOP-REAL 2); :: thesis: for n being Nat st p <> f /. 1 & f is being_S-Seq & p in LSeg (f,n) holds

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)) )

let n be Nat; :: thesis: ( p <> f /. 1 & f is being_S-Seq & p in LSeg (f,n) implies 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)) ) )

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: 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)) )

A4: f is special by A2;

A5: n <= n + 1 by NAT_1:11;

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;

( 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: verum

for n being Nat st p <> f /. 1 & f is being_S-Seq & p in LSeg (f,n) holds

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)) )

let f be FinSequence of (TOP-REAL 2); :: thesis: for n being Nat st p <> f /. 1 & f is being_S-Seq & p in LSeg (f,n) holds

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)) )

let n be Nat; :: thesis: ( p <> f /. 1 & f is being_S-Seq & p in LSeg (f,n) implies 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)) ) )

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: 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)) )

A4: f is special by A2;

A5: n <= n + 1 by NAT_1:11;

A6: now :: thesis: ( n in dom f & n + 1 in dom f )

A8:
f is one-to-one
by A2;assume A7:
( not n in dom f or not n + 1 in dom f )
; :: thesis: contradiction

end;now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( not n in dom f or not n + 1 in dom f )
by A7;

end;

suppose
not n in dom f
; :: thesis: contradiction

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: verum

end;then ( not 1 <= n or not n + 1 <= len f ) by A5, XXREAL_0:2;

hence contradiction by A3, TOPREAL1:def 3; :: thesis: verum

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

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: verum

end;hence contradiction by A3, NAT_1:11, TOPREAL1:def 3; :: thesis: verum

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: ( ( f /. n = p & f /. (n + 1) = p & contradiction ) or ( f /. n = p & f /. (n + 1) <> p & 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)) ) ) or ( f /. n <> p & f /. (n + 1) = p & 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)) ) ) or ( f /. n <> p & f /. (n + 1) <> p & 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)) ) ) )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)) ) ) or ( f /. n <> p & f /. (n + 1) = p & 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)) ) ) or ( f /. n <> p & f /. (n + 1) <> p & 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)) ) ) )

per cases
( ( f /. n = p & f /. (n + 1) = p ) or ( f /. n = p & f /. (n + 1) <> p ) or ( f /. n <> p & f /. (n + 1) = p ) or ( f /. n <> p & f /. (n + 1) <> p ) )
;

end;

case A13:
( f /. n = p & f /. (n + 1) <> p )
; :: thesis: 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)) )

( 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)) )

then
1 < n
by A1, A10, XXREAL_0:1;

then A14: 1 + 1 <= n by NAT_1:13;

( 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: verum

end;then A14: 1 + 1 <= n by NAT_1:13;

now :: thesis: 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)) )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)) )

per cases
( n = 1 + 1 or n > 2 )
by A14, XXREAL_0:1;

end;

suppose A15:
n = 1 + 1
; :: thesis: 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)) )

( 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: verum

end;

( 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)) )

now :: thesis: ex h being FinSequence of the carrier 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)) )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)) )

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

end;

suppose A16:
(f /. 1) `1 = p `1
; :: thesis: ex h being FinSequence of the carrier 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)) )

( 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)) )

take h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p*>; :: thesis: ( 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)) )

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: verum

end;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: verum

suppose A17:
(f /. 1) `2 = p `2
; :: thesis: ex h being FinSequence of the carrier 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)) )

( 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)) )

take h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*>; :: thesis: ( 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)) )

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: verum

end;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: verum

( 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: verum

suppose A18:
n > 2
; :: thesis: ex h being FinSequence of the carrier 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)) )

( 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)) )

take h = f | n; :: thesis: ( 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)) )

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: verum

end;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: verum

( 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: verum

case A19:
( f /. n <> p & f /. (n + 1) = p )
; :: thesis: 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)) )

( 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: verum

end;

( 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)) )

now :: thesis: 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)) )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)) )

per cases
( n = 1 or 1 < n )
by A10, XXREAL_0:1;

end;

suppose A20:
n = 1
; :: thesis: 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)) )

( 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: verum

end;

( 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)) )

now :: thesis: ex h being FinSequence of the carrier 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)) )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)) )

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

end;

suppose A21:
(f /. 1) `1 = p `1
; :: thesis: ex h being FinSequence of the carrier 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)) )

( 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)) )

take h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p*>; :: thesis: ( 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)) )

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, A19, A20, A21, Th15; :: thesis: verum

end;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, A19, A20, A21, Th15; :: thesis: verum

suppose A22:
(f /. 1) `2 = p `2
; :: thesis: ex h being FinSequence of the carrier 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)) )

( 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)) )

take h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*>; :: thesis: ( 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)) )

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, A19, A20, A22, Th14; :: thesis: verum

end;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, A19, A20, A22, Th14; :: thesis: verum

( 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: verum

suppose A23:
1 < n
; :: thesis: ex h being FinSequence of the carrier 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)) )

( 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)) )

take h = f | (n + 1); :: thesis: ( 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)) )

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: verum

end;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: verum

( 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: verum

case A24:
( f /. n <> p & f /. (n + 1) <> p )
; :: thesis: 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)) )

( 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: verum

end;

( 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)) )

now :: thesis: 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)) )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)) )

per cases
( n = 1 or 1 < n )
by A10, XXREAL_0:1;

end;

suppose A25:
n = 1
; :: thesis: 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)) )

( 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)) )

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;

( 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: verum

end;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: ex h being FinSequence of the carrier 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)) )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)) )

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

end;

suppose A28:
(f /. 1) `1 = (f /. (1 + 1)) `1
; :: thesis: ex h being FinSequence of the carrier 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)) )

( 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)) )

take h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + (p `2)) / 2)]|,p*>; :: thesis: ( 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)) )

( (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: verum

end;( (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: verum

suppose A29:
(f /. 1) `2 = (f /. (1 + 1)) `2
; :: thesis: ex h being FinSequence of the carrier 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)) )

( 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)) )

take h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*>; :: thesis: ( 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)) )

( (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: verum

end;( (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: verum

( 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: verum

suppose A30:
1 < n
; :: thesis: ex h being FinSequence of the carrier 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)) )

( 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)) )

take h = (f | n) ^ <*p*>; :: thesis: ( 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)) )

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: verum

end;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: verum

( 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: verum

( 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: verum