let p be Point of (TOP-REAL 2); :: thesis: for f, h being FinSequence of (TOP-REAL 2) st p <> f /. 1 & (f /. 1) `1 = p `1 & f is being_S-Seq & p in LSeg f,1 & h = <*(f /. 1),|[((f /. 1) `1 ),((((f /. 1) `2 ) + (p `2 )) / 2)]|,p*> holds
( 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 | 1)) \/ (LSeg (f /. 1),p) )
let f, h be FinSequence of (TOP-REAL 2); :: thesis: ( p <> f /. 1 & (f /. 1) `1 = p `1 & f is being_S-Seq & p in LSeg f,1 & h = <*(f /. 1),|[((f /. 1) `1 ),((((f /. 1) `2 ) + (p `2 )) / 2)]|,p*> implies ( 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 | 1)) \/ (LSeg (f /. 1),p) ) )
set p1 = f /. 1;
assume A1: ( p <> f /. 1 & (f /. 1) `1 = p `1 & f is being_S-Seq & p in LSeg f,1 & 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 | 1)) \/ (LSeg (f /. 1),p) )
then A2: len f >= 2 by TOPREAL1:def 10;
set q = f /. (1 + 1);
A3: len f >= 1 by A2, XXREAL_0:2;
A4: ( LSeg f,1 = LSeg (f /. 1),(f /. (1 + 1)) & f /. 1 in LSeg (f /. 1),(f /. (1 + 1)) ) by A2, RLTOPSP1:69, TOPREAL1:def 5;
then A5: ( LSeg (f /. 1),p c= LSeg (f /. 1),(f /. (1 + 1)) & (f /. 1) `2 <> p `2 ) by A1, TOPREAL1:12, TOPREAL3:11;
hence ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p ) by A1, TOPREAL3:43; :: thesis: ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg (f /. 1),p) )
hence L~ h is_S-P_arc_joining f /. 1,p by Def1; :: thesis: ( L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg (f /. 1),p) )
A6: ( L~ h = (LSeg (f /. 1),|[((f /. 1) `1 ),((((f /. 1) `2 ) + (p `2 )) / 2)]|) \/ (LSeg |[((f /. 1) `1 ),((((f /. 1) `2 ) + (p `2 )) / 2)]|,p) & |[((f /. 1) `1 ),((((f /. 1) `2 ) + (p `2 )) / 2)]| in LSeg (f /. 1),p ) by A1, A5, TOPREAL3:20, TOPREAL3:23;
then ( (LSeg (f /. 1),|[((f /. 1) `1 ),((((f /. 1) `2 ) + (p `2 )) / 2)]|) \/ (LSeg |[((f /. 1) `1 ),((((f /. 1) `2 ) + (p `2 )) / 2)]|,p) = LSeg (f /. 1),p & LSeg f,1 c= L~ f ) by TOPREAL1:11, TOPREAL3:26;
hence L~ h c= L~ f by A4, A5, A6, XBOOLE_1:1; :: thesis: L~ h = (L~ (f | 1)) \/ (LSeg (f /. 1),p)
A7: ( Seg 1 c= Seg (len f) & Seg (len f) = dom f & f | 1 = f | (Seg 1) ) by A3, FINSEQ_1:7, FINSEQ_1:def 3, FINSEQ_1:def 15;
then (dom f) /\ (Seg 1) = Seg 1 by XBOOLE_1:28;
then dom (f | 1) = Seg 1 by A7, RELAT_1:90;
then len (f | 1) = 1 by FINSEQ_1:def 3;
then L~ (f | 1) = {} by TOPREAL1:28;
hence L~ h = (L~ (f | 1)) \/ (LSeg (f /. 1),p) by A6, TOPREAL1:11; :: thesis: verum