let f, h be FinSequence of (TOP-REAL 2); :: thesis: ( f /. 2 <> f /. 1 & f is being_S-Seq & (f /. 2) `2 = (f /. 1) `2 & h = <*(f /. 1),|[((((f /. 1) `1 ) + ((f /. 2) `1 )) / 2),((f /. 1) `2 )]|,(f /. 2)*> implies ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. 2 & L~ h is_S-P_arc_joining f /. 1,f /. 2 & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg (f /. 1),(f /. 2)) & L~ h = (L~ (f | 2)) \/ (LSeg (f /. 2),(f /. 2)) ) )
set p1 = f /. 1;
set p = f /. 2;
assume A1: ( f /. 2 <> f /. 1 & f is being_S-Seq & (f /. 2) `2 = (f /. 1) `2 & h = <*(f /. 1),|[((((f /. 1) `1 ) + ((f /. 2) `1 )) / 2),((f /. 1) `2 )]|,(f /. 2)*> ) ; :: thesis: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. 2 & L~ h is_S-P_arc_joining f /. 1,f /. 2 & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg (f /. 1),(f /. 2)) & L~ h = (L~ (f | 2)) \/ (LSeg (f /. 2),(f /. 2)) )
then A2: len f >= 2 by TOPREAL1:def 10;
then A3: ( 1 + 1 in Seg (len f) & len f >= 1 ) by FINSEQ_1:3, XXREAL_0:2;
then A4: ( LSeg f,1 = LSeg (f /. 1),(f /. 2) & (f /. 1) `1 <> (f /. 2) `1 ) by A1, A2, TOPREAL1:def 5, TOPREAL3:11;
hence ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. 2 ) by A1, TOPREAL3:44; :: thesis: ( L~ h is_S-P_arc_joining f /. 1,f /. 2 & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg (f /. 1),(f /. 2)) & L~ h = (L~ (f | 2)) \/ (LSeg (f /. 2),(f /. 2)) )
hence A5: L~ h is_S-P_arc_joining f /. 1,f /. 2 by Def1; :: thesis: ( L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg (f /. 1),(f /. 2)) & L~ h = (L~ (f | 2)) \/ (LSeg (f /. 2),(f /. 2)) )
A6: ( L~ h = (LSeg (f /. 1),|[((((f /. 1) `1 ) + ((f /. 2) `1 )) / 2),((f /. 1) `2 )]|) \/ (LSeg |[((((f /. 1) `1 ) + ((f /. 2) `1 )) / 2),((f /. 1) `2 )]|,(f /. 2)) & |[((((f /. 1) `1 ) + ((f /. 2) `1 )) / 2),((f /. 1) `2 )]| in LSeg (f /. 1),(f /. 2) ) by A1, A4, TOPREAL3:19, TOPREAL3:23;
then A7: ( (LSeg (f /. 1),|[((((f /. 1) `1 ) + ((f /. 2) `1 )) / 2),((f /. 1) `2 )]|) \/ (LSeg |[((((f /. 1) `1 ) + ((f /. 2) `1 )) / 2),((f /. 1) `2 )]|,(f /. 2)) = LSeg (f /. 1),(f /. 2) & LSeg f,1 c= L~ f ) by TOPREAL1:11, TOPREAL3:26;
hence L~ h c= L~ f by A1, A4, TOPREAL3:23; :: thesis: ( L~ h = (L~ (f | 1)) \/ (LSeg (f /. 1),(f /. 2)) & L~ h = (L~ (f | 2)) \/ (LSeg (f /. 2),(f /. 2)) )
A8: ( 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 A8, 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),(f /. 2)) by A6, TOPREAL1:11; :: thesis: L~ h = (L~ (f | 2)) \/ (LSeg (f /. 2),(f /. 2))
A9: ( Seg 2 c= Seg (len f) & f | 2 = f | (Seg 2) ) by A2, FINSEQ_1:7, FINSEQ_1:def 15;
then (dom f) /\ (Seg 2) = Seg 2 by A8, XBOOLE_1:28;
then A10: dom (f | 2) = Seg 2 by A9, RELAT_1:90;
then A11: 1 + 1 <= len (f | 2) by FINSEQ_1:def 3;
A12: ( 1 in dom (f | 2) & 2 in dom (f | 2) ) by A10, FINSEQ_1:3;
then A13: LSeg (f | 2),1 = LSeg (f /. 1),(f /. 2) by A3, A4, A8, TOPREAL3:24;
set M = { (LSeg (f | 2),k) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | 2) ) } ;
LSeg (f /. 1),(f /. 2) in { (LSeg (f | 2),k) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | 2) ) } by A11, A13;
then ( L~ h c= L~ (f | 2) & L~ (f | 2) c= (L~ (f | 2)) \/ (LSeg (f /. 2),(f /. 2)) ) by A6, A7, XBOOLE_1:7, ZFMISC_1:92;
then A14: L~ h c= (L~ (f | 2)) \/ (LSeg (f /. 2),(f /. 2)) by XBOOLE_1:1;
(L~ (f | 2)) \/ (LSeg (f /. 2),(f /. 2)) c= L~ h

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (L~ (f | 2)) \/ (LSeg (f /. 2),(f /. 2)) or x in L~ h )
assume A15: x in (L~ (f | 2)) \/ (LSeg (f /. 2),(f /. 2)) ; :: thesis: x in L~ h

now

per cases ( x in L~ (f | 2) or x in LSeg (f /. 2),(f /. 2) ) by A15, XBOOLE_0:def 3;

suppose x in L~ (f | 2) ; :: thesis: x in L~ h

then consider X being set such that
A16: ( x in X & X in { (LSeg (f | 2),k) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | 2) ) } ) by TARSKI:def 4;
consider m being Element of NAT such that
A17: ( X = LSeg (f | 2),m & 1 <= m & m + 1 <= len (f | 2) ) by A16;
(len (f | 2)) - 1 = (1 + 1) - 1 by A10, FINSEQ_1:def 3
.= 1 ;
then (m + 1) - 1 <= 1 by A17, XREAL_1:11;
then m = 1 by A17, XXREAL_0:1;
hence x in L~ h by A3, A4, A6, A7, A8, A12, A16, A17, TOPREAL3:24; :: thesis: verum

end;

suppose x in LSeg (f /. 2),(f /. 2) ; :: thesis: x in L~ h

then ( x in {(f /. 2)} & f /. 2 in L~ h ) by A5, Th4, RLTOPSP1:71;
hence x in L~ h by TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence x in L~ h ; :: thesis: verum

end;

hence L~ h = (L~ (f | 2)) \/ (LSeg (f /. 2),(f /. 2)) by A14, XBOOLE_0:def 10; :: thesis: verum