let p be Point of (TOP-REAL 2); :: thesis: for f, h being FinSequence of (TOP-REAL 2) st p <> f /. 1 & (f /. 1) `2 = p `2 & f is being_S-Seq & p in LSeg f,1 & h = <*(f /. 1),|[((((f /. 1) `1 ) + (p `1 )) / 2),((f /. 1) `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) `2 = p `2 & f is being_S-Seq & p in LSeg f,1 & h = <*(f /. 1),|[((((f /. 1) `1 ) + (p `1 )) / 2),((f /. 1) `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) ) )
assume that
A1: p <> f /. 1 and
A2: (f /. 1) `2 = p `2 and
A3: f is being_S-Seq and
A4: p in LSeg f,1 and
A5: 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 | 1)) \/ (LSeg (f /. 1),p) )
set p1 = f /. 1;
set q = f /. (1 + 1);
A6: L~ h = (LSeg (f /. 1),|[((((f /. 1) `1 ) + (p `1 )) / 2),((f /. 1) `2 )]|) \/ (LSeg |[((((f /. 1) `1 ) + (p `1 )) / 2),((f /. 1) `2 )]|,p) by A5, TOPREAL3:23;
A7: len f >= 2 by A3, TOPREAL1:def 10;
then A8: LSeg f,1 = LSeg (f /. 1),(f /. (1 + 1)) by TOPREAL1:def 5;
A9: (f /. 1) `1 <> p `1 by A1, A2, TOPREAL3:11;
hence A10: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p ) by A2, A5, TOPREAL3:44; :: 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:69;
then A11: LSeg (f /. 1),p c= LSeg (f /. 1),(f /. (1 + 1)) by A4, A8, TOPREAL1:12;
A12: Seg (len f) = dom f by FINSEQ_1:def 3;
thus L~ h is_S-P_arc_joining f /. 1,p by A10, Def1; :: thesis: ( L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg (f /. 1),p) )
A13: LSeg f,1 c= L~ f by TOPREAL3:26;
(LSeg (f /. 1),|[((((f /. 1) `1 ) + (p `1 )) / 2),((f /. 1) `2 )]|) \/ (LSeg |[((((f /. 1) `1 ) + (p `1 )) / 2),((f /. 1) `2 )]|,p) = LSeg (f /. 1),p by A2, A9, TOPREAL1:11, TOPREAL3:19;
hence L~ h c= L~ f by A8, A11, A6, A13, XBOOLE_1:1; :: 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:7;
then ( f | 1 = f | (Seg 1) & (dom f) /\ (Seg 1) = Seg 1 ) by A12, FINSEQ_1:def 15, XBOOLE_1:28;
then dom (f | 1) = Seg 1 by 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 A2, A9, A6, TOPREAL1:11, TOPREAL3:19; :: thesis: verum