let p be Point of (TOP-REAL 2); :: thesis: for f being FinSequence of (TOP-REAL 2) st p <> f /. 1 & f is being_S-Seq & p in L~ f 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 )
let f be FinSequence of (TOP-REAL 2); :: thesis: ( p <> f /. 1 & f is being_S-Seq & p in L~ f 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 ) )
set M = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
set p1 = f /. 1;
assume that
A1: ( p <> f /. 1 & f is being_S-Seq ) and
A2: p in L~ f ; :: 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 )
consider X being set such that
A3: p in X and
A4: X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by A2, TARSKI:def 4;
consider n being Nat such that
A5: X = LSeg (f,n) and
1 <= n and
n + 1 <= len f by A4;
consider h being FinSequence of (TOP-REAL 2) such that
A6: ( 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 ) and
L~ h = (L~ (f | n)) \/ (LSeg ((f /. n),p)) by A1, A3, A5, Th17;
take h ; :: 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 )
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 ) by A6; :: thesis: verum