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 that
A1: f /. 2 <> f /. 1 and
A2: f is being_S-Seq and
A3: (f /. 2) `2 = (f /. 1) `2 and
A4: 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))) )
A5: (f /. 1) `1 <> (f /. 2) `1 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:37; :: 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 /. 2) `1)) / 2),((f /. 1) `2)]|)) \/ (LSeg (|[((((f /. 1) `1) + ((f /. 2) `1)) / 2),((f /. 1) `2)]|,(f /. 2))) = LSeg ((f /. 1),(f /. 2)) by A3, A5, TOPREAL1:5, TOPREAL3:13;
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 /. 2) `1)) / 2),((f /. 1) `2)]|)) \/ (LSeg (|[((((f /. 1) `1) + ((f /. 2) `1)) / 2),((f /. 1) `2)]|,(f /. 2))) by A4, TOPREAL3:16;
A10: len f >= 2 by A2;
then A11: 1 + 1 in Seg (len f) by FINSEQ_1:1;
then A12: LSeg (f,1) = LSeg ((f /. 1),(f /. 2)) by A10, 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 A13: dom (f | 2) = Seg 2 by RELAT_1:61;
then A14: ( 1 in dom (f | 2) & 2 in dom (f | 2) ) by FINSEQ_1:1;
thus A15: 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))) )
A16: (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 A17: 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 A17, XBOOLE_0:def 3;

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

then consider X being set such that
A18: x in X and
A19: 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
A20: X = LSeg ((f | 2),m) and
A21: 1 <= m and
A22: m + 1 <= len (f | 2) by A19;
(len (f | 2)) - 1 = (1 + 1) - 1 by A13, FINSEQ_1:def 3
.= 1 ;
then (m + 1) - 1 <= 1 by A22, XREAL_1:9;
then m = 1 by A21, XXREAL_0:1;
hence x in L~ h by A11, A12, A9, A7, A14, A18, A20, TOPREAL3:17; :: thesis: verum

end;

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

then A23: x in {(f /. 2)} by RLTOPSP1:70;
f /. 2 in L~ h by A15, Th3;
hence x in L~ h by A23, 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, A12, 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:13; :: thesis: L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2)))
A24: L~ (f | 2) c= (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) by XBOOLE_1:7;
A25: 1 + 1 <= len (f | 2) by A13, FINSEQ_1:def 3;
LSeg ((f | 2),1) = LSeg ((f /. 1),(f /. 2)) by A11, A12, A14, 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 A25;
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 A24;
hence L~ h = (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) by A16; :: thesis: verum