let p be Point of (TOP-REAL 2); :: thesis: for f, h being FinSequence of (TOP-REAL 2)

for r being Real

for u being Point of (Euclid 2) st f /. (len f) in Ball (u,r) & p in Ball (u,r) & |[((f /. (len f)) `1),(p `2)]| in Ball (u,r) & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[((f /. (len f)) `1),(p `2)]|,p*> & ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p))) /\ (L~ f) = {(f /. (len f))} holds

( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

let f, h be FinSequence of (TOP-REAL 2); :: thesis: for r being Real

for u being Point of (Euclid 2) st f /. (len f) in Ball (u,r) & p in Ball (u,r) & |[((f /. (len f)) `1),(p `2)]| in Ball (u,r) & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[((f /. (len f)) `1),(p `2)]|,p*> & ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p))) /\ (L~ f) = {(f /. (len f))} holds

( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

let r be Real; :: thesis: for u being Point of (Euclid 2) st f /. (len f) in Ball (u,r) & p in Ball (u,r) & |[((f /. (len f)) `1),(p `2)]| in Ball (u,r) & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[((f /. (len f)) `1),(p `2)]|,p*> & ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p))) /\ (L~ f) = {(f /. (len f))} holds

( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

let u be Point of (Euclid 2); :: thesis: ( f /. (len f) in Ball (u,r) & p in Ball (u,r) & |[((f /. (len f)) `1),(p `2)]| in Ball (u,r) & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[((f /. (len f)) `1),(p `2)]|,p*> & ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p))) /\ (L~ f) = {(f /. (len f))} implies ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) )

set p1 = f /. 1;

set p2 = f /. (len f);

assume that

A1: f /. (len f) in Ball (u,r) and

A2: p in Ball (u,r) and

A3: |[((f /. (len f)) `1),(p `2)]| in Ball (u,r) and

A4: f is being_S-Seq and

A5: p `1 <> (f /. (len f)) `1 and

A6: p `2 <> (f /. (len f)) `2 and

A7: h = f ^ <*|[((f /. (len f)) `1),(p `2)]|,p*> and

A8: ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p))) /\ (L~ f) = {(f /. (len f))} ; :: thesis: ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

set p3 = |[((f /. (len f)) `1),(p `2)]|;

set f1 = f ^ <*|[((f /. (len f)) `1),(p `2)]|*>;

set h1 = (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ^ <*p*>;

reconsider Lf = L~ f as non empty Subset of (TOP-REAL 2) by A8;

A9: f /. (len f) in LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|) by RLTOPSP1:68;

L~ f is_S-P_arc_joining f /. 1,f /. (len f) by A4;

then Lf is_an_arc_of f /. 1,f /. (len f) by Th2;

then f /. (len f) in L~ f by TOPREAL1:1;

then f /. (len f) in (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f) by A9, XBOOLE_0:def 4;

then A10: ( (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f) c= ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f)) \/ ((LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ f)) & {(f /. (len f))} c= (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f) ) by XBOOLE_1:7, ZFMISC_1:31;

{(f /. (len f))} = ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f)) \/ ((LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ f)) by A8, XBOOLE_1:23;

then A11: (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f) = {(f /. (len f))} by A10;

A12: len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) = (len f) + (len <*|[((f /. (len f)) `1),(p `2)]|*>) by FINSEQ_1:22

.= (len f) + 1 by FINSEQ_1:39 ;

then A13: (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) /. (len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) = |[((f /. (len f)) `1),(p `2)]| by FINSEQ_4:67;

A14: p = |[(p `1),(p `2)]| by EUCLID:53;

A15: Seg (len f) = dom f by FINSEQ_1:def 3;

len f >= 2 by A4;

then A16: 1 <= len f by XXREAL_0:2;

then len f in dom f by A15, FINSEQ_1:1;

then A17: (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) /. (len f) = f /. (len f) by FINSEQ_4:68;

A18: (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) c= {|[((f /. (len f)) `1),(p `2)]|}

.= h by A7, FINSEQ_1:def 9 ;

A31: ( |[((f /. (len f)) `1),(p `2)]| `2 = p `2 & |[((f /. (len f)) `1),(p `2)]| `1 = (f /. (len f)) `1 ) by EUCLID:52;

then A32: f ^ <*|[((f /. (len f)) `1),(p `2)]|*> is being_S-Seq by A1, A3, A4, A6, A11, Th19;

A33: L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) is_S-P_arc_joining f /. 1,|[((f /. (len f)) `1),(p `2)]| by A1, A3, A4, A6, A31, A11, Th19;

then reconsider Lf1 = L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) as non empty Subset of (TOP-REAL 2) by Th1, TOPREAL1:26;

A34: |[((f /. (len f)) `1),(p `2)]| in LSeg (|[((f /. (len f)) `1),(p `2)]|,p) by RLTOPSP1:68;

A35: (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) /. (len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) = |[((f /. (len f)) `1),(p `2)]| by A12, FINSEQ_4:67;

L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) c= (L~ f) \/ (Ball (u,r)) by A1, A3, A4, A6, A31, A11, Th19;

then (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) \/ (Ball (u,r)) c= ((L~ f) \/ (Ball (u,r))) \/ (Ball (u,r)) by XBOOLE_1:9;

then A36: (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) \/ (Ball (u,r)) c= (L~ f) \/ ((Ball (u,r)) \/ (Ball (u,r))) by XBOOLE_1:4;

A37: ( ( p `1 = |[((f /. (len f)) `1),(p `2)]| `1 & p `2 <> |[((f /. (len f)) `1),(p `2)]| `2 ) or ( p `1 <> |[((f /. (len f)) `1),(p `2)]| `1 & p `2 = |[((f /. (len f)) `1),(p `2)]| `2 ) ) by A5, EUCLID:52;

Lf1 is_an_arc_of f /. 1,|[((f /. (len f)) `1),(p `2)]| by A33, Th2;

then |[((f /. (len f)) `1),(p `2)]| in L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) by TOPREAL1:1;

then |[((f /. (len f)) `1),(p `2)]| in (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) by A34, XBOOLE_0:def 4;

then {|[((f /. (len f)) `1),(p `2)]|} c= (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) by ZFMISC_1:31;

then A38: (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) = {|[((f /. (len f)) `1),(p `2)]|} by A18;

1 in dom f by A15, A16, FINSEQ_1:1;

then (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) /. 1 = f /. 1 by FINSEQ_4:68;

hence L~ h is_S-P_arc_joining f /. 1,p by A2, A3, A37, A32, A35, A38, A30, Th19; :: thesis: L~ h c= (L~ f) \/ (Ball (u,r))

L~ ((f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ^ <*p*>) c= (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) \/ (Ball (u,r)) by A2, A3, A37, A32, A35, A38, Th19;

hence L~ h c= (L~ f) \/ (Ball (u,r)) by A30, A36; :: thesis: verum

for r being Real

for u being Point of (Euclid 2) st f /. (len f) in Ball (u,r) & p in Ball (u,r) & |[((f /. (len f)) `1),(p `2)]| in Ball (u,r) & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[((f /. (len f)) `1),(p `2)]|,p*> & ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p))) /\ (L~ f) = {(f /. (len f))} holds

( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

let f, h be FinSequence of (TOP-REAL 2); :: thesis: for r being Real

for u being Point of (Euclid 2) st f /. (len f) in Ball (u,r) & p in Ball (u,r) & |[((f /. (len f)) `1),(p `2)]| in Ball (u,r) & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[((f /. (len f)) `1),(p `2)]|,p*> & ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p))) /\ (L~ f) = {(f /. (len f))} holds

( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

let r be Real; :: thesis: for u being Point of (Euclid 2) st f /. (len f) in Ball (u,r) & p in Ball (u,r) & |[((f /. (len f)) `1),(p `2)]| in Ball (u,r) & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[((f /. (len f)) `1),(p `2)]|,p*> & ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p))) /\ (L~ f) = {(f /. (len f))} holds

( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

let u be Point of (Euclid 2); :: thesis: ( f /. (len f) in Ball (u,r) & p in Ball (u,r) & |[((f /. (len f)) `1),(p `2)]| in Ball (u,r) & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[((f /. (len f)) `1),(p `2)]|,p*> & ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p))) /\ (L~ f) = {(f /. (len f))} implies ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) )

set p1 = f /. 1;

set p2 = f /. (len f);

assume that

A1: f /. (len f) in Ball (u,r) and

A2: p in Ball (u,r) and

A3: |[((f /. (len f)) `1),(p `2)]| in Ball (u,r) and

A4: f is being_S-Seq and

A5: p `1 <> (f /. (len f)) `1 and

A6: p `2 <> (f /. (len f)) `2 and

A7: h = f ^ <*|[((f /. (len f)) `1),(p `2)]|,p*> and

A8: ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p))) /\ (L~ f) = {(f /. (len f))} ; :: thesis: ( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )

set p3 = |[((f /. (len f)) `1),(p `2)]|;

set f1 = f ^ <*|[((f /. (len f)) `1),(p `2)]|*>;

set h1 = (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ^ <*p*>;

reconsider Lf = L~ f as non empty Subset of (TOP-REAL 2) by A8;

A9: f /. (len f) in LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|) by RLTOPSP1:68;

L~ f is_S-P_arc_joining f /. 1,f /. (len f) by A4;

then Lf is_an_arc_of f /. 1,f /. (len f) by Th2;

then f /. (len f) in L~ f by TOPREAL1:1;

then f /. (len f) in (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f) by A9, XBOOLE_0:def 4;

then A10: ( (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f) c= ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f)) \/ ((LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ f)) & {(f /. (len f))} c= (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f) ) by XBOOLE_1:7, ZFMISC_1:31;

{(f /. (len f))} = ((LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f)) \/ ((LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ f)) by A8, XBOOLE_1:23;

then A11: (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (L~ f) = {(f /. (len f))} by A10;

A12: len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) = (len f) + (len <*|[((f /. (len f)) `1),(p `2)]|*>) by FINSEQ_1:22

.= (len f) + 1 by FINSEQ_1:39 ;

then A13: (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) /. (len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) = |[((f /. (len f)) `1),(p `2)]| by FINSEQ_4:67;

A14: p = |[(p `1),(p `2)]| by EUCLID:53;

A15: Seg (len f) = dom f by FINSEQ_1:def 3;

len f >= 2 by A4;

then A16: 1 <= len f by XXREAL_0:2;

then len f in dom f by A15, FINSEQ_1:1;

then A17: (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) /. (len f) = f /. (len f) by FINSEQ_4:68;

A18: (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) c= {|[((f /. (len f)) `1),(p `2)]|}

proof

A30: (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ^ <*p*> =
f ^ (<*|[((f /. (len f)) `1),(p `2)]|*> ^ <*p*>)
by FINSEQ_1:32
set M1 = { (LSeg ((f ^ <*|[((f /. (len f)) `1),(p `2)]|*>),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ) } ;

set Mf = { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } ;

assume not (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) c= {|[((f /. (len f)) `1),(p `2)]|} ; :: thesis: contradiction

then consider x being object such that

A19: x in (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) and

A20: not x in {|[((f /. (len f)) `1),(p `2)]|} ;

x in L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) by A19, XBOOLE_0:def 4;

then consider X being set such that

A21: x in X and

A22: X in { (LSeg ((f ^ <*|[((f /. (len f)) `1),(p `2)]|*>),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ) } by TARSKI:def 4;

consider k being Nat such that

A23: X = LSeg ((f ^ <*|[((f /. (len f)) `1),(p `2)]|*>),k) and

A24: 1 <= k and

A25: k + 1 <= len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) by A22;

A26: x in LSeg (|[((f /. (len f)) `1),(p `2)]|,p) by A19, XBOOLE_0:def 4;

end;set Mf = { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } ;

assume not (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) c= {|[((f /. (len f)) `1),(p `2)]|} ; :: thesis: contradiction

then consider x being object such that

A19: x in (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) and

A20: not x in {|[((f /. (len f)) `1),(p `2)]|} ;

x in L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) by A19, XBOOLE_0:def 4;

then consider X being set such that

A21: x in X and

A22: X in { (LSeg ((f ^ <*|[((f /. (len f)) `1),(p `2)]|*>),i)) where i is Nat : ( 1 <= i & i + 1 <= len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ) } by TARSKI:def 4;

consider k being Nat such that

A23: X = LSeg ((f ^ <*|[((f /. (len f)) `1),(p `2)]|*>),k) and

A24: 1 <= k and

A25: k + 1 <= len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) by A22;

A26: x in LSeg (|[((f /. (len f)) `1),(p `2)]|,p) by A19, XBOOLE_0:def 4;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( k + 1 = len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) or k + 1 < len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) )
by A25, XXREAL_0:1;

end;

suppose
k + 1 = len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)
; :: thesis: contradiction

then
LSeg ((f ^ <*|[((f /. (len f)) `1),(p `2)]|*>),k) = LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)
by A12, A13, A17, A24, TOPREAL1:def 3;

then x in (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) by A26, A21, A23, XBOOLE_0:def 4;

hence contradiction by A20, TOPREAL3:29; :: thesis: verum

end;then x in (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) /\ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) by A26, A21, A23, XBOOLE_0:def 4;

hence contradiction by A20, TOPREAL3:29; :: thesis: verum

suppose
k + 1 < len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)
; :: thesis: contradiction

then A27:
k + 1 <= len f
by A12, NAT_1:13;

k <= k + 1 by NAT_1:11;

then k <= len f by A27, XXREAL_0:2;

then A28: k in dom f by A15, A24, FINSEQ_1:1;

1 <= k + 1 by A24, NAT_1:13;

then k + 1 in dom f by A15, A27, FINSEQ_1:1;

then X = LSeg (f,k) by A23, A28, TOPREAL3:18;

then X in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A24, A27;

then A29: x in L~ f by A21, TARSKI:def 4;

x in (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) by A26, XBOOLE_0:def 3;

then x in {(f /. (len f))} by A8, A29, XBOOLE_0:def 4;

then x = f /. (len f) by TARSKI:def 1;

hence contradiction by A6, A14, A26, TOPREAL3:12; :: thesis: verum

end;k <= k + 1 by NAT_1:11;

then k <= len f by A27, XXREAL_0:2;

then A28: k in dom f by A15, A24, FINSEQ_1:1;

1 <= k + 1 by A24, NAT_1:13;

then k + 1 in dom f by A15, A27, FINSEQ_1:1;

then X = LSeg (f,k) by A23, A28, TOPREAL3:18;

then X in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A24, A27;

then A29: x in L~ f by A21, TARSKI:def 4;

x in (LSeg ((f /. (len f)),|[((f /. (len f)) `1),(p `2)]|)) \/ (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) by A26, XBOOLE_0:def 3;

then x in {(f /. (len f))} by A8, A29, XBOOLE_0:def 4;

then x = f /. (len f) by TARSKI:def 1;

hence contradiction by A6, A14, A26, TOPREAL3:12; :: thesis: verum

.= h by A7, FINSEQ_1:def 9 ;

A31: ( |[((f /. (len f)) `1),(p `2)]| `2 = p `2 & |[((f /. (len f)) `1),(p `2)]| `1 = (f /. (len f)) `1 ) by EUCLID:52;

then A32: f ^ <*|[((f /. (len f)) `1),(p `2)]|*> is being_S-Seq by A1, A3, A4, A6, A11, Th19;

A33: L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) is_S-P_arc_joining f /. 1,|[((f /. (len f)) `1),(p `2)]| by A1, A3, A4, A6, A31, A11, Th19;

then reconsider Lf1 = L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) as non empty Subset of (TOP-REAL 2) by Th1, TOPREAL1:26;

A34: |[((f /. (len f)) `1),(p `2)]| in LSeg (|[((f /. (len f)) `1),(p `2)]|,p) by RLTOPSP1:68;

A35: (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) /. (len (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) = |[((f /. (len f)) `1),(p `2)]| by A12, FINSEQ_4:67;

L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) c= (L~ f) \/ (Ball (u,r)) by A1, A3, A4, A6, A31, A11, Th19;

then (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) \/ (Ball (u,r)) c= ((L~ f) \/ (Ball (u,r))) \/ (Ball (u,r)) by XBOOLE_1:9;

then A36: (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) \/ (Ball (u,r)) c= (L~ f) \/ ((Ball (u,r)) \/ (Ball (u,r))) by XBOOLE_1:4;

A37: ( ( p `1 = |[((f /. (len f)) `1),(p `2)]| `1 & p `2 <> |[((f /. (len f)) `1),(p `2)]| `2 ) or ( p `1 <> |[((f /. (len f)) `1),(p `2)]| `1 & p `2 = |[((f /. (len f)) `1),(p `2)]| `2 ) ) by A5, EUCLID:52;

Lf1 is_an_arc_of f /. 1,|[((f /. (len f)) `1),(p `2)]| by A33, Th2;

then |[((f /. (len f)) `1),(p `2)]| in L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) by TOPREAL1:1;

then |[((f /. (len f)) `1),(p `2)]| in (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) by A34, XBOOLE_0:def 4;

then {|[((f /. (len f)) `1),(p `2)]|} c= (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) by ZFMISC_1:31;

then A38: (LSeg (|[((f /. (len f)) `1),(p `2)]|,p)) /\ (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) = {|[((f /. (len f)) `1),(p `2)]|} by A18;

1 in dom f by A15, A16, FINSEQ_1:1;

then (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) /. 1 = f /. 1 by FINSEQ_4:68;

hence L~ h is_S-P_arc_joining f /. 1,p by A2, A3, A37, A32, A35, A38, A30, Th19; :: thesis: L~ h c= (L~ f) \/ (Ball (u,r))

L~ ((f ^ <*|[((f /. (len f)) `1),(p `2)]|*>) ^ <*p*>) c= (L~ (f ^ <*|[((f /. (len f)) `1),(p `2)]|*>)) \/ (Ball (u,r)) by A2, A3, A37, A32, A35, A38, Th19;

hence L~ h c= (L~ f) \/ (Ball (u,r)) by A30, A36; :: thesis: verum