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 A1: ( 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*> ) ; :: 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 p1 = f /. 1;
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) `1 <> p `1 ) by A1, TOPREAL1:12, TOPREAL3:11;
hence ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p ) by A1, 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) )
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 ) + (p `1 )) / 2),((f /. 1) `2 )]|) \/ (LSeg |[((((f /. 1) `1 ) + (p `1 )) / 2),((f /. 1) `2 )]|,p) & |[((((f /. 1) `1 ) + (p `1 )) / 2),((f /. 1) `2 )]| in LSeg (f /. 1),p ) by A1, A5, TOPREAL3:19, TOPREAL3:23;
then ( (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 & 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