let f, h be FinSequence of (TOP-REAL 2); :: thesis: ( f /. 2 <> f /. 1 & f is being_S-Seq & (f /. 2) `1 = (f /. 1) `1 & h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + ((f /. 2) `2)) / 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 that
A1: f /. 2 <> f /. 1 and
A2: f is being_S-Seq and
A3: (f /. 2) `1 = (f /. 1) `1 and
A4: h = <*(f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + ((f /. 2) `2)) / 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))) )
A5: (f /. 1) `2 <> (f /. 2) `2 by A1, A3, TOPREAL3:6;
hence A6: ( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = f /. 2 ) by A3, A4, TOPREAL3:36; :: 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))) )
A7: (LSeg ((f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + ((f /. 2) `2)) / 2)]|)) \/ (LSeg (|[((f /. 1) `1),((((f /. 1) `2) + ((f /. 2) `2)) / 2)]|,(f /. 2))) = LSeg ((f /. 1),(f /. 2)) by A3, A5, TOPREAL1:5, TOPREAL3:14;
set M = { (LSeg ((f | 2),k)) where k is Nat : ( 1 <= k & k + 1 <= len (f | 2) ) } ;
A8: Seg (len f) = dom f by FINSEQ_1:def 3;
A9: L~ h = (LSeg ((f /. 1),|[((f /. 1) `1),((((f /. 1) `2) + ((f /. 2) `2)) / 2)]|)) \/ (LSeg (|[((f /. 1) `1),((((f /. 1) `2) + ((f /. 2) `2)) / 2)]|,(f /. 2))) by A4, TOPREAL3:16;
A10: len f >= 1 + 1 by A2;
then A11: LSeg (f,1) = LSeg ((f /. 1),(f /. 2)) by TOPREAL1:def 3;
Seg 2 c= Seg (len f) by A10, FINSEQ_1:5;
then ( f | 2 = f | (Seg 2) & (dom f) /\ (Seg 2) = Seg 2 ) by A8, FINSEQ_1:def 16, XBOOLE_1:28;
then A12: dom (f | 2) = Seg 2 by RELAT_1:61;
then A13: ( 1 in dom (f | 2) & 2 in dom (f | 2) ) by FINSEQ_1:1;
thus A14: L~ h is_S-P_arc_joining f /. 1,f /. 2 by A6; :: 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))) )
A15: (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) c= L~ h

proof

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

now :: thesis: x in L~ h

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

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

then consider X being set such that
A17: x in X and
A18: X in { (LSeg ((f | 2),k)) where k is Nat : ( 1 <= k & k + 1 <= len (f | 2) ) } by TARSKI:def 4;
consider m being Nat such that
A19: X = LSeg ((f | 2),m) and
A20: 1 <= m and
A21: m + 1 <= len (f | 2) by A18;
(len (f | 2)) - 1 = (1 + 1) - 1 by A12, FINSEQ_1:def 3
.= 1 ;
then (m + 1) - 1 <= 1 by A21, XREAL_1:9;
then m = 1 by A20, XXREAL_0:1;
hence x in L~ h by A10, A11, A9, A7, A13, A17, A19, TOPREAL3:17; :: thesis: verum

end;

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

then A22: x in {(f /. 2)} by RLTOPSP1:70;
f /. 2 in L~ h by A14, Th3;
hence x in L~ h by A22, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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

end;

LSeg (f,1) c= L~ f by TOPREAL3:19;
hence L~ h c= L~ f by A4, A11, A7, TOPREAL3:16; :: thesis: ( L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),(f /. 2))) & L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) )
len f >= 1 by A10, 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 A8, 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),(f /. 2))) by A3, A5, A9, TOPREAL1:5, TOPREAL3:14; :: thesis: L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2)))
A23: L~ (f | 2) c= (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) by XBOOLE_1:7;
A24: 1 + 1 <= len (f | 2) by A12, FINSEQ_1:def 3;
LSeg ((f | 2),1) = LSeg ((f /. 1),(f /. 2)) by A10, A11, A13, TOPREAL3:17;
then LSeg ((f /. 1),(f /. 2)) in { (LSeg ((f | 2),k)) where k is Nat : ( 1 <= k & k + 1 <= len (f | 2) ) } by A24;
then L~ h c= L~ (f | 2) by A9, A7, ZFMISC_1:74;
then L~ h c= (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) by A23;
hence L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) by A15; :: thesis: verum