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 ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> holds
( h is being_S-Seq & 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 ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> holds
( h is being_S-Seq & 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 ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> holds
( h is being_S-Seq & 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); ( ( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) ) & f /. (len f) in Ball (u,r) & p in Ball (u,r) & f is being_S-Seq & (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} & h = f ^ <*p*> implies ( h is being_S-Seq & 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:
( ( p `1 = (f /. (len f)) `1 & p `2 <> (f /. (len f)) `2 ) or ( p `1 <> (f /. (len f)) `1 & p `2 = (f /. (len f)) `2 ) )
; ( not f /. (len f) in Ball (u,r) or not p in Ball (u,r) or not f is being_S-Seq or not (LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))} or not h = f ^ <*p*> or ( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) ) )
assume that
A2:
( f /. (len f) in Ball (u,r) & p in Ball (u,r) )
and
A3:
f is being_S-Seq
and
A4:
(LSeg ((f /. (len f)),p)) /\ (L~ f) = {(f /. (len f))}
and
A5:
h = f ^ <*p*>
; ( h is being_S-Seq & L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )
A6:
not p in L~ f
by A1, A4, TOPREAL3:40;
A7:
f is one-to-one
by A3;
A8:
f is unfolded
by A3;
A9:
f is one-to-one
by A3;
A10:
f is s.n.c.
by A3;
A11:
Seg (len h) = dom h
by FINSEQ_1:def 3;
set Mf = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
set Mh = { (LSeg (h,m)) where m is Nat : ( 1 <= m & m + 1 <= len h ) } ;
A12:
Seg (len f) = dom f
by FINSEQ_1:def 3;
A13:
2 <= len f
by A3;
then A14:
1 <= len f
by XXREAL_0:2;
then A15:
len f in dom f
by A12, FINSEQ_1:1;
then A16:
h /. (len f) = f /. (len f)
by A5, FINSEQ_4:68;
A17: len h =
(len f) + (len <*p*>)
by A5, FINSEQ_1:22
.=
(len f) + 1
by FINSEQ_1:39
;
then A18:
h /. (len h) = p
by A5, FINSEQ_4:67;
then A19:
LSeg (h,(len f)) = LSeg ((f /. (len f)),p)
by A17, A14, A16, TOPREAL1:def 3;
A20:
f is special
by A3;
thus A21:
h is being_S-Seq
( L~ h is_S-P_arc_joining f /. 1,p & L~ h c= (L~ f) \/ (Ball (u,r)) )proof
now for x, y being object holds
( not x in dom h or not y in dom h or not h . x = h . y or not x <> y )set Z =
{ m where m is Nat : ( 1 <= m & m <= len h ) } ;
given x,
y being
object such that A22:
x in dom h
and A23:
y in dom h
and A24:
h . x = h . y
and A25:
x <> y
;
contradiction
y in { m where m is Nat : ( 1 <= m & m <= len h ) }
by A11, A23, FINSEQ_1:def 1;
then consider k2 being
Nat such that A26:
k2 = y
and A27:
1
<= k2
and A28:
k2 <= len h
;
x in { m where m is Nat : ( 1 <= m & m <= len h ) }
by A11, A22, FINSEQ_1:def 1;
then consider k1 being
Nat such that A29:
k1 = x
and A30:
1
<= k1
and A31:
k1 <= len h
;
A32:
h /. k1 =
h . y
by A22, A24, A29, PARTFUN1:def 6
.=
h /. k2
by A23, A26, PARTFUN1:def 6
;
now contradictionper cases
( ( k1 = (len f) + 1 & k2 = (len f) + 1 ) or ( k1 = (len f) + 1 & k2 < (len f) + 1 ) or ( k1 < (len f) + 1 & k2 = (len f) + 1 ) or ( k1 < (len f) + 1 & k2 < (len f) + 1 ) )
by A17, A31, A28, XXREAL_0:1;
suppose A33:
(
k1 = (len f) + 1 &
k2 < (len f) + 1 )
;
contradictionthen A34:
k2 + 1
<= k1
by NAT_1:13;
now contradictionper cases
( k2 + 1 = k1 or k2 + 1 < k1 )
by A34, XXREAL_0:1;
suppose
k2 + 1
< k1
;
contradictionthen A35:
k2 < ((len f) + 1) - 1
by A33, XREAL_1:20;
reconsider k2 =
k2 as
Element of
NAT by ORDINAL1:def 12;
k2 in dom f
by A12, A27, A35, FINSEQ_1:1;
then
h /. k2 = f /. k2
by A5, FINSEQ_4:68;
hence
contradiction
by A5, A13, A6, A27, A32, A33, A35, FINSEQ_4:67, TOPREAL3:39;
verum end; end; end; hence
contradiction
;
verum end; suppose A36:
(
k1 < (len f) + 1 &
k2 = (len f) + 1 )
;
contradictionthen A37:
k1 + 1
<= k2
by NAT_1:13;
now contradictionper cases
( k1 + 1 = k2 or k1 + 1 < k2 )
by A37, XXREAL_0:1;
suppose
k1 + 1
< k2
;
contradictionthen A38:
k1 < ((len f) + 1) - 1
by A36, XREAL_1:20;
reconsider k1 =
k1 as
Element of
NAT by ORDINAL1:def 12;
k1 in dom f
by A12, A30, A38, FINSEQ_1:1;
then
h /. k1 = f /. k1
by A5, FINSEQ_4:68;
hence
contradiction
by A5, A13, A6, A30, A32, A36, A38, FINSEQ_4:67, TOPREAL3:39;
verum end; end; end; hence
contradiction
;
verum end; suppose A39:
(
k1 < (len f) + 1 &
k2 < (len f) + 1 )
;
contradictionthen
k2 <= len f
by NAT_1:13;
then A40:
k2 in dom f
by A12, A27, FINSEQ_1:1;
k1 <= len f
by A39, NAT_1:13;
then A41:
k1 in dom f
by A12, A30, FINSEQ_1:1;
then f . k1 =
h . k1
by A5, FINSEQ_1:def 7
.=
f . k2
by A5, A24, A29, A26, A40, FINSEQ_1:def 7
;
hence
contradiction
by A9, A25, A29, A26, A41, A40, FUNCT_1:def 4;
verum end; end; end; hence
contradiction
;
verum end;
hence
h is
one-to-one
by FUNCT_1:def 4;
TOPREAL1:def 8 ( 2 <= len h & h is unfolded & h is s.n.c. & h is special )
2
+ 1
<= (len f) + 1
by A13, XREAL_1:6;
hence
len h >= 2
by A17, XXREAL_0:2;
( h is unfolded & h is s.n.c. & h is special )
thus
h is
unfolded
( h is s.n.c. & h is special )proof
let j be
Nat;
TOPREAL1:def 6 ( not 1 <= j or not j + 2 <= len h or (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))} )
assume that A42:
1
<= j
and A43:
j + 2
<= len h
;
(LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}
A44:
j + (1 + 1) = (j + 1) + 1
;
j + 1
<= j + 2
by XREAL_1:6;
then A45:
j + 1
<= len h
by A43, XXREAL_0:2;
now (LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}per cases
( j + 2 = len h or j + 2 < len h )
by A43, XXREAL_0:1;
suppose A46:
j + 2
= len h
;
(LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}then A47:
j + ((1 + 1) - 1) = len f
by A17;
then
j <= len f
by NAT_1:13;
then
j in dom f
by A12, A42, FINSEQ_1:1;
then A48:
LSeg (
h,
j)
= LSeg (
f,
j)
by A5, A15, A47, TOPREAL3:18;
LSeg (
h,
j)
in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
by A42, A47, A48;
then A49:
LSeg (
h,
j)
= (LSeg (h,j)) /\ (L~ f)
by XBOOLE_1:28, ZFMISC_1:74;
h /. (j + 1) in LSeg (
h,
j)
by A42, A45, TOPREAL1:21;
then A50:
{(h /. (j + 1))} c= LSeg (
h,
j)
by ZFMISC_1:31;
LSeg (
h,
(j + 1))
= LSeg (
(f /. (len f)),
p)
by A17, A14, A18, A16, A46, TOPREAL1:def 3;
hence (LSeg (h,j)) /\ (LSeg (h,(j + 1))) =
(LSeg (h,j)) /\ {(h /. (j + 1))}
by A4, A17, A16, A46, A49, XBOOLE_1:16
.=
{(h /. (j + 1))}
by A50, XBOOLE_1:28
;
verum end; suppose
j + 2
< len h
;
(LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}then A51:
(j + (2 + 1)) - 1
<= len f
by A17, NAT_1:13;
then A52:
(LSeg (f,j)) /\ (LSeg (f,(j + 1))) = {(f /. (j + 1))}
by A8, A42, A43;
1
<= j + 2
by A44, NAT_1:11;
then A53:
(j + 1) + 1
in dom f
by A12, A51, FINSEQ_1:1;
j + 1
<= j + 2
by A44, NAT_1:11;
then A54:
j + 1
<= len f
by A51, XXREAL_0:2;
1
<= j + 1
by NAT_1:11;
then A55:
j + 1
in dom f
by A12, A54, FINSEQ_1:1;
then A56:
h /. (j + 1) = f /. (j + 1)
by A5, FINSEQ_4:68;
j <= j + 1
by NAT_1:11;
then
j <= len f
by A54, XXREAL_0:2;
then
j in dom f
by A12, A42, FINSEQ_1:1;
then
LSeg (
h,
j)
= LSeg (
f,
j)
by A5, A55, TOPREAL3:18;
hence
(LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}
by A5, A52, A55, A53, A56, TOPREAL3:18;
verum end; end; end;
hence
(LSeg (h,j)) /\ (LSeg (h,(j + 1))) = {(h /. (j + 1))}
;
verum
end;
thus
h is
s.n.c.
h is special proof
let n,
m be
Nat;
TOPREAL1:def 7 ( m <= n + 1 or LSeg (h,n) misses LSeg (h,m) )
assume A57:
m > n + 1
;
LSeg (h,n) misses LSeg (h,m)
n <= n + 1
by NAT_1:11;
then A58:
n <= m
by A57, XXREAL_0:2;
A59:
(n + 1) + 1
= n + (1 + 1)
;
A60:
1
<= n + 1
by NAT_1:11;
LSeg (
f,
n)
misses LSeg (
f,
m)
by A10, A57;
then A61:
(LSeg (f,n)) /\ (LSeg (f,m)) = {}
;
now (LSeg (h,n)) /\ (LSeg (h,m)) = {} per cases
( m + 1 < len h or m + 1 = len h or m + 1 > len h )
by XXREAL_0:1;
suppose A62:
m + 1
< len h
;
(LSeg (h,n)) /\ (LSeg (h,m)) = {} then A63:
m + 1
<= len f
by A17, NAT_1:13;
A64:
1
< m
by A57, A60, XXREAL_0:2;
then
1
<= m + 1
by NAT_1:13;
then A65:
m + 1
in dom f
by A12, A63, FINSEQ_1:1;
A66:
m <= len f
by A17, A62, XREAL_1:6;
then
m in dom f
by A12, A64, FINSEQ_1:1;
then A67:
LSeg (
h,
m)
= LSeg (
f,
m)
by A5, A65, TOPREAL3:18;
now (LSeg (h,n)) /\ (LSeg (h,m)) = {} per cases
( 0 < n or 0 = n )
;
suppose
0 < n
;
(LSeg (h,n)) /\ (LSeg (h,m)) = {} then A68:
0 + 1
<= n
by NAT_1:13;
n + 1
<= len f
by A57, A66, XXREAL_0:2;
then A69:
n + 1
in dom f
by A12, A60, FINSEQ_1:1;
n <= len f
by A58, A66, XXREAL_0:2;
then
n in dom f
by A12, A68, FINSEQ_1:1;
hence
(LSeg (h,n)) /\ (LSeg (h,m)) = {}
by A5, A61, A67, A69, TOPREAL3:18;
verum end; end; end; hence
(LSeg (h,n)) /\ (LSeg (h,m)) = {}
;
verum end; suppose A70:
m + 1
= len h
;
(LSeg (h,n)) /\ (LSeg (h,m)) = {} now (LSeg (h,n)) /\ (LSeg (h,m)) = {} per cases
( 0 < n or 0 = n )
;
suppose A71:
0 < n
;
(LSeg (h,n)) /\ (LSeg (h,m)) = {} A72:
n + 1
in dom f
by A17, A12, A57, A60, A70, FINSEQ_1:1;
A73:
0 + 1
<= n
by A71, NAT_1:13;
then
n in dom f
by A17, A12, A58, A70, FINSEQ_1:1;
then A74:
LSeg (
h,
n)
= LSeg (
f,
n)
by A5, A72, TOPREAL3:18;
now not (LSeg (h,n)) /\ (LSeg (h,m)) <> {} set L =
LSeg (
f,
n);
set x = the
Element of
(LSeg (h,n)) /\ (LSeg (h,m));
assume A75:
(LSeg (h,n)) /\ (LSeg (h,m)) <> {}
;
contradictionthen A76:
the
Element of
(LSeg (h,n)) /\ (LSeg (h,m)) in LSeg (
f,
n)
by A74, XBOOLE_0:def 4;
A77:
the
Element of
(LSeg (h,n)) /\ (LSeg (h,m)) in LSeg (
(f /. (len f)),
p)
by A17, A19, A70, A75, XBOOLE_0:def 4;
LSeg (
f,
n)
in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
by A17, A57, A70, A73;
then
the
Element of
(LSeg (h,n)) /\ (LSeg (h,m)) in L~ f
by A76, TARSKI:def 4;
then
the
Element of
(LSeg (h,n)) /\ (LSeg (h,m)) in {(f /. (len f))}
by A4, A77, XBOOLE_0:def 4;
then A78:
the
Element of
(LSeg (h,n)) /\ (LSeg (h,m)) = f /. (len f)
by TARSKI:def 1;
A79:
(n + 1) + 1
<= len f
by A17, A57, A70, NAT_1:13;
now contradictionper cases
( (n + 1) + 1 = len f or (n + 1) + 1 < len f )
by A79, XXREAL_0:1;
suppose A80:
(n + 1) + 1
= len f
;
contradiction
1
<= n + 1
by NAT_1:11;
then A81:
f /. (len f) in LSeg (
f,
(n + 1))
by A80, TOPREAL1:21;
(LSeg (f,n)) /\ (LSeg (f,(n + 1))) = {(f /. (n + 1))}
by A8, A59, A73, A80;
then
f /. (len f) in {(f /. (n + 1))}
by A76, A78, A81, XBOOLE_0:def 4;
then
f /. (len f) = f /. (n + 1)
by TARSKI:def 1;
then
(len f) + 1
= len f
by A15, A7, A72, A80, PARTFUN2:10;
hence
contradiction
;
verum end; suppose A82:
(n + 1) + 1
< len f
;
contradictionreconsider j =
(len f) - 1 as
Element of
NAT by A13, INT_1:5, XXREAL_0:2;
(n + 2) + 1
<= len f
by A82, NAT_1:13;
then
n + 2
<= (len f) - 1
by XREAL_1:19;
then
n + 1
< j
by A59, NAT_1:13;
then
LSeg (
f,
n)
misses LSeg (
f,
j)
by A10;
then A83:
(LSeg (f,n)) /\ (LSeg (f,j)) = {}
;
(1 + 1) - 1
= 1
;
then
(
j + 1
= len f & 1
<= j )
by A13, XREAL_1:13;
then
f /. (len f) in LSeg (
f,
j)
by TOPREAL1:21;
hence
contradiction
by A76, A78, A83, XBOOLE_0:def 4;
verum end; end; end; hence
contradiction
;
verum end; hence
(LSeg (h,n)) /\ (LSeg (h,m)) = {}
;
verum end; end; end; hence
(LSeg (h,n)) /\ (LSeg (h,m)) = {}
;
verum end; end; end;
hence
(LSeg (h,n)) /\ (LSeg (h,m)) = {}
;
XBOOLE_0:def 7 verum
end;
hereby TOPREAL1:def 5 verum
let n be
Nat;
( 1 <= n & n + 1 <= len h & not (h /. n) `1 = (h /. (n + 1)) `1 implies (h /. n) `2 = (h /. (n + 1)) `2 )assume that A84:
1
<= n
and A85:
n + 1
<= len h
;
( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )set p3 =
h /. n;
set p4 =
h /. (n + 1);
now ( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )per cases
( n + 1 = len h or n + 1 < len h )
by A85, XXREAL_0:1;
suppose A86:
n + 1
< len h
;
( (h /. n) `1 = (h /. (n + 1)) `1 or (h /. n) `2 = (h /. (n + 1)) `2 )A87:
1
<= n + 1
by A84, NAT_1:13;
n + 1
<= len f
by A17, A86, NAT_1:13;
then
n + 1
in dom f
by A12, A87, FINSEQ_1:1;
then A88:
h /. (n + 1) = f /. (n + 1)
by A5, FINSEQ_4:68;
n <= len f
by A17, A86, XREAL_1:6;
then
n in dom f
by A12, A84, FINSEQ_1:1;
then A89:
h /. n = f /. n
by A5, FINSEQ_4:68;
n + 1
<= len f
by A17, A86, NAT_1:13;
hence
(
(h /. n) `1 = (h /. (n + 1)) `1 or
(h /. n) `2 = (h /. (n + 1)) `2 )
by A20, A84, A89, A88;
verum end; end; end; hence
(
(h /. n) `1 = (h /. (n + 1)) `1 or
(h /. n) `2 = (h /. (n + 1)) `2 )
;
verum
end;
end;
1 in dom f
by A12, A14, FINSEQ_1:1;
then
h /. 1 = f /. 1
by A5, FINSEQ_4:68;
hence
L~ h is_S-P_arc_joining f /. 1,p
by A18, A21; L~ h c= (L~ f) \/ (Ball (u,r))
let x be object ; TARSKI:def 3 ( not x in L~ h or x in (L~ f) \/ (Ball (u,r)) )
assume
x in L~ h
; x in (L~ f) \/ (Ball (u,r))
then consider X being set such that
A90:
x in X
and
A91:
X in { (LSeg (h,m)) where m is Nat : ( 1 <= m & m + 1 <= len h ) }
by TARSKI:def 4;
consider k being Nat such that
A92:
X = LSeg (h,k)
and
A93:
1 <= k
and
A94:
k + 1 <= len h
by A91;
per cases
( k + 1 = len h or k + 1 < len h )
by A94, XXREAL_0:1;
suppose A95:
k + 1
= len h
;
x in (L~ f) \/ (Ball (u,r))A96:
Ball (
u,
r)
c= (L~ f) \/ (Ball (u,r))
by XBOOLE_1:7;
X c= Ball (
u,
r)
by A2, A17, A19, A92, A95, TOPREAL3:21;
hence
x in (L~ f) \/ (Ball (u,r))
by A90, A96;
verum end; suppose
k + 1
< len h
;
x in (L~ f) \/ (Ball (u,r))then A97:
k + 1
<= len f
by A17, NAT_1:13;
k <= k + 1
by NAT_1:11;
then
k <= len f
by A97, XXREAL_0:2;
then A98:
k in dom f
by A12, A93, FINSEQ_1:1;
1
<= k + 1
by A93, NAT_1:13;
then
k + 1
in dom f
by A12, A97, FINSEQ_1:1;
then
X = LSeg (
f,
k)
by A5, A92, A98, TOPREAL3:18;
then
X in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
by A93, A97;
then
x in union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) }
by A90, TARSKI:def 4;
hence
x in (L~ f) \/ (Ball (u,r))
by XBOOLE_0:def 3;
verum end; end;