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 that
A1: p <> f /. 1 and
A2: (f /. 1) `1 = p `1 and
A3: f is being_S-Seq and
A4: p in LSeg (f,1) and
A5: 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)) )
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)) by A5, TOPREAL3:16;
set q = f /. (1 + 1);
A7: len f >= 2 by A3;
then A8: LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1))) by TOPREAL1:def 3;
A9: (f /. 1) `2 <> p `2 by A1, A2, TOPREAL3:6;
hence A10: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p ) by A2, A5, TOPREAL3:36; :: 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)) )
f /. 1 in LSeg ((f /. 1),(f /. (1 + 1))) by RLTOPSP1:68;
then A11: LSeg ((f /. 1),p) c= LSeg ((f /. 1),(f /. (1 + 1))) by A4, A8, TOPREAL1:6;
A12: Seg (len f) = dom f by FINSEQ_1:def 3;
thus L~ h is_S-P_arc_joining f /. 1,p by A10; :: thesis: ( L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) )
A13: LSeg (f,1) c= L~ f by TOPREAL3:19;
(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) by A2, A9, TOPREAL1:5, TOPREAL3:14;
hence L~ h c= L~ f by A8, A11, A6, A13; :: thesis: L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p))
len f >= 1 by A7, XXREAL_0:2;
then Seg 1 c= Seg (len f) by FINSEQ_1:5;
then ( f | 1 = f | (Seg 1) & (dom f) /\ (Seg 1) = Seg 1 ) by A12, FINSEQ_1:def 16, XBOOLE_1:28;
then dom (f | 1) = Seg 1 by RELAT_1:61;
then len (f | 1) = 1 by FINSEQ_1:def 3;
then L~ (f | 1) = {} by TOPREAL1:22;
hence L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) by A2, A9, A6, TOPREAL1:5, TOPREAL3:14; :: thesis: verum