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