let p be Point of (TOP-REAL 2); 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); ( 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 that
A1:
p <> f /. 1
and
A2:
(f /. 1) `2 = p `2
and
A3:
f is being_S-Seq
and
A4:
p in LSeg (f,1)
and
A5:
h = <*(f /. 1),|[((((f /. 1) `1) + (p `1)) / 2),((f /. 1) `2)]|,p*>
; ( 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)) )
set p1 = f /. 1;
set q = f /. (1 + 1);
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))
by A5, TOPREAL3:16;
A7:
len f >= 2
by A3;
then A8:
LSeg (f,1) = LSeg ((f /. 1),(f /. (1 + 1)))
by TOPREAL1:def 3;
A9:
(f /. 1) `1 <> p `1
by A1, A2, TOPREAL3:6;
hence A10:
( h is being_S-Seq & h /. 1 = f /. 1 & h /. (len h) = p )
by A2, A5, TOPREAL3:37; ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) )
f /. 1 in LSeg ((f /. 1),(f /. (1 + 1)))
by RLTOPSP1:68;
then A11:
LSeg ((f /. 1),p) c= LSeg ((f /. 1),(f /. (1 + 1)))
by A4, A8, TOPREAL1:6;
A12:
Seg (len f) = dom f
by FINSEQ_1:def 3;
thus
L~ h is_S-P_arc_joining f /. 1,p
by A10; ( L~ h c= L~ f & L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p)) )
A13:
LSeg (f,1) c= L~ f
by TOPREAL3:19;
(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)
by A2, A9, TOPREAL1:5, TOPREAL3:13;
hence
L~ h c= L~ f
by A8, A11, A6, A13; L~ h = (L~ (f | 1)) \/ (LSeg ((f /. 1),p))
len f >= 1
by A7, 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 A12, 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),p))
by A2, A9, A6, TOPREAL1:5, TOPREAL3:13; verum