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 & |[(p `1 ),((f /. (len f)) `2 )]| in Ball u,r & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|,p*> & ((LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) \/ (LSeg |[(p `1 ),((f /. (len f)) `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 & |[(p `1 ),((f /. (len f)) `2 )]| in Ball u,r & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|,p*> & ((LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) \/ (LSeg |[(p `1 ),((f /. (len f)) `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 & |[(p `1 ),((f /. (len f)) `2 )]| in Ball u,r & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|,p*> & ((LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) \/ (LSeg |[(p `1 ),((f /. (len f)) `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 & |[(p `1 ),((f /. (len f)) `2 )]| in Ball u,r & f is being_S-Seq & p `1 <> (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 & h = f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|,p*> & ((LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) \/ (LSeg |[(p `1 ),((f /. (len f)) `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: |[(p `1 ),((f /. (len f)) `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 ^ <*|[(p `1 ),((f /. (len f)) `2 )]|,p*> and
A8: ((LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) \/ (LSeg |[(p `1 ),((f /. (len f)) `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 = |[(p `1 ),((f /. (len f)) `2 )]|;
set f1 = f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>;
set h1 = (f ^ <*|[(p `1 ),((f /. (len f)) `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)),|[(p `1 ),((f /. (len f)) `2 )]| by RLTOPSP1:69;
L~ f is_S-P_arc_joining f /. 1,f /. (len f) by A4, Def1;
then Lf is_an_arc_of f /. 1,f /. (len f) by Th3;
then f /. (len f) in L~ f by TOPREAL1:4;
then f /. (len f) in (LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) /\ (L~ f) by A9, XBOOLE_0:def 4;
then A10: ( (LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) /\ (L~ f) c= ((LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) /\ (L~ f)) \/ ((LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p) /\ (L~ f)) & {(f /. (len f))} c= (LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) /\ (L~ f) ) by XBOOLE_1:7, ZFMISC_1:37;
{(f /. (len f))} = ((LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) /\ (L~ f)) \/ ((LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p) /\ (L~ f)) by A8, XBOOLE_1:23;
then A11: (LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) /\ (L~ f) = {(f /. (len f))} by A10, XBOOLE_0:def 10;
A12: len (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) = (len f) + (len <*|[(p `1 ),((f /. (len f)) `2 )]|*>) by FINSEQ_1:35
.= (len f) + 1 by FINSEQ_1:56 ;
then A13: (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) /. (len (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) = |[(p `1 ),((f /. (len f)) `2 )]| by FINSEQ_4:82;
A14: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
A15: Seg (len f) = dom f by FINSEQ_1:def 3;
len f >= 2 by A4, TOPREAL1:def 10;
then A16: 1 <= len f by XXREAL_0:2;
then len f in dom f by A15, FINSEQ_1:3;
then A17: (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) /. (len f) = f /. (len f) by FINSEQ_4:83;
A18: (LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p) /\ (L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) c= {|[(p `1 ),((f /. (len f)) `2 )]|}

proof

set M1 = { (LSeg (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) ) } ;
set Mf = { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ;
assume not (LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p) /\ (L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) c= {|[(p `1 ),((f /. (len f)) `2 )]|} ; :: thesis: contradiction
then consider x being set such that
A19: x in (LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p) /\ (L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) and
A20: not x in {|[(p `1 ),((f /. (len f)) `2 )]|} by TARSKI:def 3;
x in L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) by A19, XBOOLE_0:def 4;
then consider X being set such that
A21: x in X and
A22: X in { (LSeg (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>),i) where i is Element of NAT : ( 1 <= i & i + 1 <= len (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) ) } by TARSKI:def 4;
consider k being Element of NAT such that
A23: X = LSeg (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>),k and
A24: 1 <= k and
A25: k + 1 <= len (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) by A22;
A26: x in LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p by A19, XBOOLE_0:def 4;

now

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

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

then LSeg (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>),k = LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]| by A12, A13, A17, A24, TOPREAL1:def 5;
then x in (LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) /\ (LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p) by A26, A21, A23, XBOOLE_0:def 4;
hence contradiction by A20, TOPREAL3:37; :: thesis: verum

end;

suppose k + 1 < len (f ^ <*|[(p `1 ),((f /. (len f)) `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:3;
1 <= k + 1 by A24, NAT_1:13;
then k + 1 in dom f by A15, A27, FINSEQ_1:3;
then X = LSeg f,k by A23, A28, TOPREAL3:25;
then X in { (LSeg f,j) where j is Element of 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)),|[(p `1 ),((f /. (len f)) `2 )]|) \/ (LSeg |[(p `1 ),((f /. (len f)) `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 A5, A14, A26, TOPREAL3:17; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

A30: (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) ^ <*p*> = f ^ (<*|[(p `1 ),((f /. (len f)) `2 )]|*> ^ <*p*>) by FINSEQ_1:45
.= h by A7, FINSEQ_1:def 9 ;
A31: ( |[(p `1 ),((f /. (len f)) `2 )]| `2 = (f /. (len f)) `2 & |[(p `1 ),((f /. (len f)) `2 )]| `1 = p `1 ) by EUCLID:56;
then A32: f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*> is being_S-Seq by A1, A3, A4, A5, A11, Th20;
A33: L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) is_S-P_arc_joining f /. 1,|[(p `1 ),((f /. (len f)) `2 )]| by A1, A3, A4, A5, A31, A11, Th20;
then reconsider Lf1 = L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) as non empty Subset of (TOP-REAL 2) by Th2, TOPREAL1:32;
A34: |[(p `1 ),((f /. (len f)) `2 )]| in LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p by RLTOPSP1:69;
A35: (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) /. (len (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) = |[(p `1 ),((f /. (len f)) `2 )]| by A12, FINSEQ_4:82;
L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) c= (L~ f) \/ (Ball u,r) by A1, A3, A4, A5, A31, A11, Th20;
then (L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) \/ (Ball u,r) c= ((L~ f) \/ (Ball u,r)) \/ (Ball u,r) by XBOOLE_1:9;
then A36: (L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) \/ (Ball u,r) c= (L~ f) \/ ((Ball u,r) \/ (Ball u,r)) by XBOOLE_1:4;
A37: ( ( p `1 = |[(p `1 ),((f /. (len f)) `2 )]| `1 & p `2 <> |[(p `1 ),((f /. (len f)) `2 )]| `2 ) or ( p `1 <> |[(p `1 ),((f /. (len f)) `2 )]| `1 & p `2 = |[(p `1 ),((f /. (len f)) `2 )]| `2 ) ) by A6, EUCLID:56;
Lf1 is_an_arc_of f /. 1,|[(p `1 ),((f /. (len f)) `2 )]| by A33, Th3;
then |[(p `1 ),((f /. (len f)) `2 )]| in L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) by TOPREAL1:4;
then |[(p `1 ),((f /. (len f)) `2 )]| in (LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p) /\ (L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) by A34, XBOOLE_0:def 4;
then {|[(p `1 ),((f /. (len f)) `2 )]|} c= (LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p) /\ (L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) by ZFMISC_1:37;
then A38: (LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p) /\ (L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) = {|[(p `1 ),((f /. (len f)) `2 )]|} by A18, XBOOLE_0:def 10;
1 in dom f by A15, A16, FINSEQ_1:3;
then (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) /. 1 = f /. 1 by FINSEQ_4:83;
hence L~ h is_S-P_arc_joining f /. 1,p by A2, A3, A37, A32, A35, A38, A30, Th20; :: thesis: L~ h c= (L~ f) \/ (Ball u,r)
L~ ((f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) ^ <*p*>) c= (L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) \/ (Ball u,r) by A2, A3, A37, A32, A35, A38, Th20;
hence L~ h c= (L~ f) \/ (Ball u,r) by A30, A36, XBOOLE_1:1; :: thesis: verum