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 not f /. 1 in Ball u,r & 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 not f /. 1 in Ball u,r & 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 not f /. 1 in Ball u,r & 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: ( not f /. 1 in Ball u,r & 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 A1:
( not f /. 1 in Ball u,r & 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))} )
; :: 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*>;
A2:
( |[(p `1 ),((f /. (len f)) `2 )]| `2 = (f /. (len f)) `2 & |[(p `1 ),((f /. (len f)) `2 )]| `1 = p `1 & p = |[(p `1 ),(p `2 )]| )
by EUCLID:56, EUCLID:57;
A3:
( {(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)) & (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)) )
by A1, XBOOLE_1:7, XBOOLE_1:23;
reconsider Lf = L~ f as non empty Subset of (TOP-REAL 2) by A1;
L~ f is_S-P_arc_joining f /. 1,f /. (len f)
by A1, Def1;
then
Lf is_an_arc_of f /. 1,f /. (len f)
by Th3;
then
( f /. (len f) in L~ f & f /. (len f) in LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]| )
by RLTOPSP1:69, TOPREAL1:4;
then
f /. (len f) in (LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) /\ (L~ f)
by XBOOLE_0:def 4;
then
{(f /. (len f))} c= (LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) /\ (L~ f)
by ZFMISC_1:37;
then A4:
(LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) /\ (L~ f) = {(f /. (len f))}
by A3, XBOOLE_0:def 10;
then A5:
( L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) is_S-P_arc_joining f /. 1,|[(p `1 ),((f /. (len f)) `2 )]| & L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) c= (L~ f) \/ (Ball u,r) )
by A1, A2, Th20;
A6:
( Seg (len f) = dom f & len f >= 2 )
by A1, FINSEQ_1:def 3, TOPREAL1:def 10;
then A7:
1 <= len f
by XXREAL_0:2;
then A8:
1 in dom f
by A6, FINSEQ_1:3;
reconsider Lf1 = L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) as non empty Subset of (TOP-REAL 2) by A5, Th2, TOPREAL1:32;
A9: 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 A10:
( (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) /. (len (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) = |[(p `1 ),((f /. (len f)) `2 )]| & Lf1 is_an_arc_of f /. 1,|[(p `1 ),((f /. (len f)) `2 )]| )
by A5, Th3, FINSEQ_4:82;
then
( |[(p `1 ),((f /. (len f)) `2 )]| in L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) & |[(p `1 ),((f /. (len f)) `2 )]| in LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p )
by RLTOPSP1:69, 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 XBOOLE_0:def 4;
then A11:
( {|[(p `1 ),((f /. (len f)) `2 )]|} c= (LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p) /\ (L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) & len f in dom f )
by A6, A7, FINSEQ_1:3, ZFMISC_1:37;
then A12:
(f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) /. (len f) = f /. (len f)
by FINSEQ_4:83;
(LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p) /\ (L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) c= {|[(p `1 ),((f /. (len f)) `2 )]|}
proof
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 A13:
(
x in (LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p) /\ (L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) & not
x in {|[(p `1 ),((f /. (len f)) `2 )]|} )
by TARSKI:def 3;
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 ) } ;
A14:
(
x in LSeg |[(p `1 ),((f /. (len f)) `2 )]|,
p &
x in L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) )
by A13, XBOOLE_0:def 4;
then consider X being
set such that A15:
(
x in X &
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 A16:
(
X = LSeg (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>),
k & 1
<= k &
k + 1
<= len (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) )
by A15;
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 A16, XXREAL_0:1;
suppose
k + 1
= len (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)
;
:: thesis: contradictionthen
LSeg (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>),
k = LSeg (f /. (len f)),
|[(p `1 ),((f /. (len f)) `2 )]|
by A9, A10, A12, A16, TOPREAL1:def 5;
then
(
x in (LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) /\ (LSeg |[(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) = {|[(p `1 ),((f /. (len f)) `2 )]|} )
by A14, A15, A16, TOPREAL3:37, XBOOLE_0:def 4;
hence
contradiction
by A13;
:: thesis: verum end; suppose A17:
k + 1
< len (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)
;
:: thesis: contradictionthen A18:
(
k + 1
< (len f) + 1 &
k <= k + 1 )
by A9, NAT_1:11;
A19:
(
k + 1
<= len f & 1
<= k + 1 )
by A9, A16, A17, NAT_1:13;
then A20:
(
k + 1
in dom f &
k <= len f )
by A6, A18, FINSEQ_1:3, XXREAL_0:2;
then
k in dom f
by A6, A16, FINSEQ_1:3;
then
X = LSeg f,
k
by A16, A20, TOPREAL3:25;
then
X in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) }
by A16, A19;
then
(
x in (LSeg (f /. (len f)),|[(p `1 ),((f /. (len f)) `2 )]|) \/ (LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p) &
x in L~ f )
by A14, A15, TARSKI:def 4, XBOOLE_0:def 3;
then
x in {(f /. (len f))}
by A1, XBOOLE_0:def 4;
then
x = f /. (len f)
by TARSKI:def 1;
hence
contradiction
by A1, A2, A14, TOPREAL3:17;
:: thesis: verum end;
hence
contradiction
;
:: thesis: verum
end;
then A21:
( ( ( 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 ) ) & not f /. 1 in Ball u,r & |[(p `1 ),((f /. (len f)) `2 )]| in Ball u,r & p in Ball u,r & f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*> is being_S-Seq & (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) /. 1 = f /. 1 & (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) /. (len (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) = |[(p `1 ),((f /. (len f)) `2 )]| & (LSeg |[(p `1 ),((f /. (len f)) `2 )]|,p) /\ (L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) = {|[(p `1 ),((f /. (len f)) `2 )]|} )
by A1, A2, A4, A8, A9, A11, Th20, FINSEQ_4:82, FINSEQ_4:83, XBOOLE_0:def 10;
then A22:
L~ ((f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) ^ <*p*>) c= (L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) \/ (Ball u,r)
by Th20;
A23: (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>) ^ <*p*> =
f ^ (<*|[(p `1 ),((f /. (len f)) `2 )]|*> ^ <*p*>)
by FINSEQ_1:45
.=
h
by A1, FINSEQ_1:def 9
;
hence
L~ h is_S-P_arc_joining f /. 1,p
by A21, Th20; :: thesis: L~ h c= (L~ f) \/ (Ball u,r)
(L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) \/ (Ball u,r) c= ((L~ f) \/ (Ball u,r)) \/ (Ball u,r)
by A5, XBOOLE_1:9;
then
(L~ (f ^ <*|[(p `1 ),((f /. (len f)) `2 )]|*>)) \/ (Ball u,r) c= (L~ f) \/ ((Ball u,r) \/ (Ball u,r))
by XBOOLE_1:4;
hence
L~ h c= (L~ f) \/ (Ball u,r)
by A22, A23, XBOOLE_1:1; :: thesis: verum