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 15, 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

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 15, 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

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 15, 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

LSeg (f,1) c= L~ f
by TOPREAL3:19;
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

end;assume A17: x in (L~ (f | 2)) \/ (LSeg ((f /. 2),(f /. 2))) ; :: thesis: x in L~ h

now :: thesis: x in L~ hend;

hence
x in L~ h
; :: thesis: verumper cases
( x in L~ (f | 2) or x in LSeg ((f /. 2),(f /. 2)) )
by A17, XBOOLE_0:def 3;

end;

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;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

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 15, 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