let p be Point of (TOP-REAL 2); 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); 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; 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); ( 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))}
; ( 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: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)),|[(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:31;
{(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;
A12: len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) =
(len f) + (len <*|[(p `1),((f /. (len f)) `2)]|*>)
by FINSEQ_1:22
.=
(len f) + 1
by FINSEQ_1:39
;
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: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 ^ <*|[(p `1),((f /. (len f)) `2)]|*>) /. (len f) = f /. (len f)
by FINSEQ_4:68;
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 Nat : ( 1 <= i & i + 1 <= len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ) } ;
set Mf =
{ (LSeg (f,j)) where j is 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)]|}
;
contradiction
then consider x being
object 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)]|}
;
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 Nat : ( 1 <= i & i + 1 <= len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ) }
by TARSKI:def 4;
consider k being
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 contradictionper 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)]|*>)
;
contradictionthen
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 3;
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:30;
verum end; suppose
k + 1
< len (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)
;
contradictionthen 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)),|[(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:11;
verum end;
hence
contradiction
;
verum
end;
A30: (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) ^ <*p*> =
f ^ (<*|[(p `1),((f /. (len f)) `2)]|*> ^ <*p*>)
by FINSEQ_1:32
.=
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:52;
then A32:
f ^ <*|[(p `1),((f /. (len f)) `2)]|*> is being_S-Seq
by A1, A3, A4, A5, A11, Th19;
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, Th19;
then reconsider Lf1 = L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) as non empty Subset of (TOP-REAL 2) by Th1, TOPREAL1:26;
A34:
|[(p `1),((f /. (len f)) `2)]| in LSeg (|[(p `1),((f /. (len f)) `2)]|,p)
by RLTOPSP1:68;
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:67;
L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>) c= (L~ f) \/ (Ball (u,r))
by A1, A3, A4, A5, A31, A11, Th19;
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:52;
Lf1 is_an_arc_of f /. 1,|[(p `1),((f /. (len f)) `2)]|
by A33, Th2;
then
|[(p `1),((f /. (len f)) `2)]| in L~ (f ^ <*|[(p `1),((f /. (len f)) `2)]|*>)
by TOPREAL1:1;
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:31;
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;
1 in dom f
by A15, A16, FINSEQ_1:1;
then
(f ^ <*|[(p `1),((f /. (len f)) `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; 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, Th19;
hence
L~ h c= (L~ f) \/ (Ball (u,r))
by A30, A36; verum