:: UNIFORM1 semantic presentation

REAL is non empty non finite set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K6(REAL)
K6(REAL) is non empty set
NAT is non empty epsilon-transitive epsilon-connected ordinal set
K6(NAT) is non empty set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
K7(1,1) is non empty set
K6(K7(1,1)) is non empty set
K7(K7(1,1),1) is non empty set
K6(K7(K7(1,1),1)) is non empty set
K7(K7(1,1),REAL) is non empty set
K6(K7(K7(1,1),REAL)) is non empty set
K7(REAL,REAL) is non empty set
K7(K7(REAL,REAL),REAL) is non empty set
K6(K7(K7(REAL,REAL),REAL)) is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
K7(2,2) is non empty set
K7(K7(2,2),REAL) is non empty set
K6(K7(K7(2,2),REAL)) is non empty set
K254() is non empty strict TopSpace-like T_2 compact V116() TopStruct
the carrier of K254() is non empty V181() set
RealSpace is non empty strict Reflexive discerning V86() triangle Discerning V116() MetrStruct
R^1 is non empty strict TopSpace-like V116() TopStruct
K6(NAT) is non empty set
COMPLEX is non empty non finite set
RAT is non empty non finite set
INT is non empty non finite set
K6(K7(REAL,REAL)) is non empty set
TOP-REAL 2 is non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() L15()
the carrier of (TOP-REAL 2) is non empty set
K298( the carrier of (TOP-REAL 2)) is non empty functional FinSequence-membered M16( the carrier of (TOP-REAL 2))
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered Element of NAT
Closed-Interval-TSpace (0,1) is non empty strict V116() SubSpace of R^1
Seg 1 is non empty finite V43(1) Element of K6(NAT)
n is V11() real ext-real Element of REAL
1 / n is V11() real ext-real Element of REAL
n " is V11() real ext-real set
1 * (n ") is V11() real ext-real set
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
e * n is V11() real ext-real Element of REAL
(1 / n) * n is V11() real ext-real Element of REAL
1 / e is V11() real ext-real non negative Element of REAL
e " is V11() real ext-real non negative set
1 * (e ") is V11() real ext-real non negative set
n is non empty MetrStruct
the carrier of n is non empty set
e is non empty MetrStruct
the carrier of e is non empty set
K7( the carrier of n, the carrier of e) is non empty set
K6(K7( the carrier of n, the carrier of e)) is non empty set
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
e is non empty Reflexive discerning V86() triangle Discerning MetrStruct
TopSpaceMetr e is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr e) is non empty set
K7( the carrier of n, the carrier of (TopSpaceMetr e)) is non empty set
K6(K7( the carrier of n, the carrier of (TopSpaceMetr e))) is non empty set
the carrier of e is non empty set
K6( the carrier of (TopSpaceMetr e)) is non empty set
g is non empty V19() V22( the carrier of n) V23( the carrier of (TopSpaceMetr e)) Function-like total V33( the carrier of n, the carrier of (TopSpaceMetr e)) Element of K6(K7( the carrier of n, the carrier of (TopSpaceMetr e)))
p1 is V11() real ext-real Element of REAL
p2 is Element of the carrier of e
Ball (p2,p1) is Element of K6( the carrier of e)
K6( the carrier of e) is non empty set
h is Element of K6( the carrier of (TopSpaceMetr e))
g " h is Element of K6( the carrier of n)
K6( the carrier of n) is non empty set
[#] (TopSpaceMetr e) is non empty non proper Element of K6( the carrier of (TopSpaceMetr e))
f is Element of K6( the carrier of (TopSpaceMetr e))
n is non empty Reflexive discerning V86() triangle Discerning MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr n) is non empty set
e is non empty Reflexive discerning V86() triangle Discerning MetrStruct
TopSpaceMetr e is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr e) is non empty set
K7( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e)) is non empty set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e))) is non empty set
the carrier of n is non empty set
the carrier of e is non empty set
g is non empty V19() V22( the carrier of (TopSpaceMetr n)) V23( the carrier of (TopSpaceMetr e)) Function-like total V33( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e)) Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e)))
dom g is Element of K6( the carrier of (TopSpaceMetr n))
K6( the carrier of (TopSpaceMetr n)) is non empty set
K6( the carrier of (TopSpaceMetr e)) is non empty set
p1 is V11() real ext-real set
p2 is Element of the carrier of e
Ball (p2,p1) is Element of K6( the carrier of e)
K6( the carrier of e) is non empty set
h is Element of K6( the carrier of (TopSpaceMetr e))
g " h is Element of K6( the carrier of (TopSpaceMetr n))
s1 is Element of the carrier of n
g . s1 is set
f is Element of K6( the carrier of (TopSpaceMetr e))
s is Element of the carrier of e
j is V11() real ext-real set
Ball (s,j) is Element of K6( the carrier of e)
p is V11() real ext-real Element of REAL
h1 is V11() real ext-real set
y is V11() real ext-real Element of REAL
Ball (s1,y) is Element of K6( the carrier of n)
K6( the carrier of n) is non empty set
x is set
nx is Element of the carrier of n
g . nx is set
rng g is Element of K6( the carrier of (TopSpaceMetr e))
dist (s1,nx) is V11() real ext-real Element of REAL
ry is Element of the carrier of e
dist (s,ry) is V11() real ext-real Element of REAL
Ball (s,p) is Element of K6( the carrier of e)
p1 is V11() real ext-real set
h is Element of the carrier of e
p2 is Element of the carrier of n
g . p2 is set
n is non empty Reflexive discerning V86() triangle Discerning MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr n) is non empty set
e is non empty Reflexive discerning V86() triangle Discerning MetrStruct
TopSpaceMetr e is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr e) is non empty set
K7( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e)) is non empty set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e))) is non empty set
the carrier of n is non empty set
the carrier of e is non empty set
g is non empty V19() V22( the carrier of (TopSpaceMetr n)) V23( the carrier of (TopSpaceMetr e)) Function-like total V33( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e)) Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e)))
p1 is V11() real ext-real Element of REAL
p2 is Element of the carrier of n
g . p2 is set
h is Element of the carrier of e
K6( the carrier of (TopSpaceMetr e)) is non empty set
Ball (h,p1) is Element of K6( the carrier of e)
K6( the carrier of e) is non empty set
dom g is Element of K6( the carrier of (TopSpaceMetr n))
K6( the carrier of (TopSpaceMetr n)) is non empty set
f is Element of K6( the carrier of (TopSpaceMetr e))
g " f is Element of K6( the carrier of (TopSpaceMetr n))
s1 is V11() real ext-real set
Ball (p2,s1) is Element of K6( the carrier of n)
K6( the carrier of n) is non empty set
s is V11() real ext-real Element of REAL
j is Element of the carrier of n
g . j is set
dist (p2,j) is V11() real ext-real Element of REAL
p is Element of the carrier of e
dist (h,p) is V11() real ext-real Element of REAL
Ball (p2,s) is Element of K6( the carrier of n)
n is non empty Reflexive discerning V86() triangle Discerning MetrStruct
the carrier of n is non empty set
e is non empty Reflexive discerning V86() triangle Discerning MetrStruct
the carrier of e is non empty set
K7( the carrier of n, the carrier of e) is non empty set
K6(K7( the carrier of n, the carrier of e)) is non empty set
TopSpaceMetr n is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr n) is non empty set
TopSpaceMetr e is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr e) is non empty set
K7( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e)) is non empty set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e))) is non empty set
g is non empty V19() V22( the carrier of n) V23( the carrier of e) Function-like total V33( the carrier of n, the carrier of e) Element of K6(K7( the carrier of n, the carrier of e))
p1 is non empty V19() V22( the carrier of (TopSpaceMetr n)) V23( the carrier of (TopSpaceMetr e)) Function-like total V33( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e)) Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e)))
p2 is V11() real ext-real set
h is Element of the carrier of n
p1 . h is set
f is Element of the carrier of e
s1 is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
j is Element of the carrier of n
p1 . j is set
dist (h,j) is V11() real ext-real Element of REAL
p is Element of the carrier of e
dist (f,p) is V11() real ext-real Element of REAL
g /. h is Element of the carrier of e
g . h is Element of the carrier of e
g /. j is Element of the carrier of e
g . j is Element of the carrier of e
n is non empty Reflexive discerning V86() triangle Discerning MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
K6(K6( the carrier of (TopSpaceMetr n))) is non empty set
the carrier of n is non empty set
e is Element of K6(K6( the carrier of (TopSpaceMetr n)))
Family_open_set n is Element of K6(K6( the carrier of n))
K6( the carrier of n) is non empty set
K6(K6( the carrier of n)) is non empty set
TopStruct(# the carrier of n,(Family_open_set n) #) is strict TopStruct
p1 is set
p2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
1 / (p2 + 1) is V11() real ext-real non negative Element of REAL
(p2 + 1) " is non empty V11() real ext-real positive non negative set
1 * ((p2 + 1) ") is V11() real ext-real non negative set
f is Element of the carrier of n
s1 is Element of the carrier of n
dist (f,s1) is V11() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
j is Element of the carrier of n
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
1 / (s + 1) is V11() real ext-real non negative Element of REAL
(s + 1) " is non empty V11() real ext-real positive non negative set
1 * ((s + 1) ") is V11() real ext-real non negative set
K7(NAT, the carrier of n) is non empty set
K6(K7(NAT, the carrier of n)) is non empty set
p1 is non empty V19() V22( NAT ) V23( the carrier of n) Function-like total V33( NAT , the carrier of n) Element of K6(K7(NAT, the carrier of n))
p1 is non empty V19() V22( NAT ) V23( the carrier of n) Function-like total V33( NAT , the carrier of n) Element of K6(K7(NAT, the carrier of n))
p2 is Element of K6(K6( the carrier of (TopSpaceMetr n)))
{ b₁ where b₁ is Element of the carrier of n : S₃[b₁] } is set
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
{ b₁ where b₁ is Element of the carrier of n : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT st
( f <= b₂ & b₁ = p1 . b₂ ) } is set
p1 . f is Element of the carrier of n
s1 is Element of K6(K6( the carrier of (TopSpaceMetr n)))
clf s1 is Element of K6(K6( the carrier of (TopSpaceMetr n)))
f is Element of K6( the carrier of (TopSpaceMetr n))
Cl f is Element of K6( the carrier of (TopSpaceMetr n))
j is set
meet j is set
p is Element of K6(K6( the carrier of (TopSpaceMetr n)))
h1 is set
y is set
x is Element of K6( the carrier of (TopSpaceMetr n))
nx is Element of K6( the carrier of (TopSpaceMetr n))
Cl nx is Element of K6( the carrier of (TopSpaceMetr n))
ry is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
{ b₁ where b₁ is Element of the carrier of n : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT st
( ry <= b₂ & b₁ = p1 . b₂ ) } is set
y is Element of K6( the carrier of (TopSpaceMetr n))
x3 is Element of K6( the carrier of (TopSpaceMetr n))
Cl x3 is Element of K6( the carrier of (TopSpaceMetr n))
x3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
{ b₁ where b₁ is Element of the carrier of n : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT st
( x3 <= b₂ & b₁ = p1 . b₂ ) } is set
r3 is set
y3 is Element of the carrier of n
y3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p1 . y3 is Element of the carrier of n
y3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p1 . y3 is Element of the carrier of n
r3 is set
y3 is Element of the carrier of n
y3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p1 . y3 is Element of the carrier of n
y3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p1 . y3 is Element of the carrier of n
h1 is set
meet p is Element of K6( the carrier of (TopSpaceMetr n))
y is Element of K6( the carrier of (TopSpaceMetr n))
x is Element of K6( the carrier of (TopSpaceMetr n))
Cl x is Element of K6( the carrier of (TopSpaceMetr n))
meet (clf s1) is Element of K6( the carrier of (TopSpaceMetr n))
j is Element of the carrier of (TopSpaceMetr n)
p is Element of the carrier of n
h1 is Element of K6( the carrier of (TopSpaceMetr n))
y is Element of K6( the carrier of (TopSpaceMetr n))
x is V11() real ext-real set
Ball (p,x) is Element of K6( the carrier of n)
nx is V11() real ext-real Element of REAL
nx / 2 is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative set
nx * (2 ") is V11() real ext-real set
ry is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
1 / ry is V11() real ext-real non negative Element of REAL
ry " is V11() real ext-real non negative set
1 * (ry ") is V11() real ext-real non negative set
Ball (p,(nx / 2)) is Element of K6( the carrier of n)
y is Element of K6( the carrier of (TopSpaceMetr n))
{ b₁ where b₁ is Element of the carrier of (TopSpaceMetr n) : S₄[b₁] } is set
x3 is Element of K6( the carrier of (TopSpaceMetr n))
Cl x3 is Element of K6( the carrier of (TopSpaceMetr n))
x3 is set
r3 is Element of the carrier of n
dist (p,r3) is V11() real ext-real Element of REAL
ry + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
1 / (ry + 1) is V11() real ext-real non negative Element of REAL
(ry + 1) " is non empty V11() real ext-real positive non negative set
1 * ((ry + 1) ") is V11() real ext-real non negative set
y3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p1 . y3 is Element of the carrier of n
y3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p1 . y3 is Element of the carrier of n
y3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
1 / (y3 + 1) is V11() real ext-real non negative Element of REAL
(y3 + 1) " is non empty V11() real ext-real positive non negative set
1 * ((y3 + 1) ") is V11() real ext-real non negative set
y3 is Element of the carrier of n
dist (r3,y3) is V11() real ext-real Element of REAL
(nx / 2) + (nx / 2) is V11() real ext-real Element of REAL
(nx / 2) + (dist (r3,y3)) is V11() real ext-real Element of REAL
nx / 1 is V11() real ext-real Element of REAL
1 " is non empty V11() real ext-real positive non negative set
nx * (1 ") is V11() real ext-real set
Ball (p,nx) is Element of K6( the carrier of n)
dist (p,y3) is V11() real ext-real Element of REAL
(dist (p,r3)) + (dist (r3,y3)) is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V86() triangle Discerning MetrStruct
the carrier of n is non empty set
e is non empty Reflexive discerning V86() triangle Discerning MetrStruct
the carrier of e is non empty set
K7( the carrier of n, the carrier of e) is non empty set
K6(K7( the carrier of n, the carrier of e)) is non empty set
TopSpaceMetr n is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr n) is non empty set
TopSpaceMetr e is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr e) is non empty set
K7( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e)) is non empty set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e))) is non empty set
g is non empty V19() V22( the carrier of n) V23( the carrier of e) Function-like total V33( the carrier of n, the carrier of e) Element of K6(K7( the carrier of n, the carrier of e))
p1 is non empty V19() V22( the carrier of (TopSpaceMetr n)) V23( the carrier of (TopSpaceMetr e)) Function-like total V33( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e)) Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of (TopSpaceMetr e)))
p2 is V11() real ext-real Element of REAL
K6( the carrier of (TopSpaceMetr n)) is non empty set
p2 / 2 is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative set
p2 * (2 ") is V11() real ext-real set
{ b₁ where b₁ is Element of K6( the carrier of (TopSpaceMetr n)) : ex b₂ being Element of the carrier of n ex b₃ being V11() real ext-real Element of REAL st
( b₁ = Ball (b₂,b₃) & ( for b₄ being Element of the carrier of n
for b₅, b₆ being Element of the carrier of e holds
( not b₅ = g . b₂ or not b₆ = g . b₄ or b₃ <= dist (b₂,b₄) or not p2 / 2 <= dist (b₅,b₆) ) ) ) } is set
bool the carrier of n is non empty Element of K6(K6( the carrier of n))
K6( the carrier of n) is non empty set
K6(K6( the carrier of n)) is non empty set
f is set
s1 is Element of K6( the carrier of (TopSpaceMetr n))
s is Element of the carrier of n
j is V11() real ext-real Element of REAL
Ball (s,j) is Element of K6( the carrier of n)
g . s is Element of the carrier of e
K6(K6( the carrier of (TopSpaceMetr n))) is non empty set
f is Element of K6(K6( the carrier of (TopSpaceMetr n)))
s1 is Element of K6( the carrier of (TopSpaceMetr n))
s is Element of K6( the carrier of (TopSpaceMetr n))
j is Element of the carrier of n
p is V11() real ext-real Element of REAL
Ball (j,p) is Element of K6( the carrier of n)
g . j is Element of the carrier of e
union f is Element of K6( the carrier of (TopSpaceMetr n))
s1 is set
s is Element of the carrier of n
p1 . s is set
g /. s is Element of the carrier of e
g . s is Element of the carrier of e
j is Element of the carrier of e
p is V11() real ext-real Element of REAL
Ball (s,p) is Element of K6( the carrier of n)
x is Element of the carrier of e
nx is Element of the carrier of e
y is Element of the carrier of n
g . y is Element of the carrier of e
dist (s,y) is V11() real ext-real Element of REAL
dist (x,nx) is V11() real ext-real Element of REAL
h1 is Element of K6( the carrier of (TopSpaceMetr n))
y is Element of the carrier of n
x is V11() real ext-real Element of REAL
Ball (y,x) is Element of K6( the carrier of n)
g . y is Element of the carrier of e
s1 is V11() real ext-real Element of REAL
s is Element of the carrier of n
j is Element of the carrier of n
dist (s,j) is V11() real ext-real Element of REAL
g /. s is Element of the carrier of e
g . s is Element of the carrier of e
g /. j is Element of the carrier of e
g . j is Element of the carrier of e
dist ((g /. s),(g /. j)) is V11() real ext-real Element of REAL
p is Element of K6( the carrier of (TopSpaceMetr n))
h1 is Element of K6( the carrier of (TopSpaceMetr n))
y is Element of the carrier of n
x is V11() real ext-real Element of REAL
Ball (y,x) is Element of K6( the carrier of n)
g . y is Element of the carrier of e
y is Element of the carrier of n
x is V11() real ext-real Element of REAL
Ball (y,x) is Element of K6( the carrier of n)
g . y is Element of the carrier of e
dist (y,j) is V11() real ext-real Element of REAL
g /. y is Element of the carrier of e
dist ((g /. y),(g /. j)) is V11() real ext-real Element of REAL
dist (y,s) is V11() real ext-real Element of REAL
dist ((g /. y),(g /. s)) is V11() real ext-real Element of REAL
dist ((g /. s),(g /. y)) is V11() real ext-real Element of REAL
(dist ((g /. s),(g /. y))) + (dist ((g /. y),(g /. j))) is V11() real ext-real Element of REAL
(p2 / 2) + (p2 / 2) is V11() real ext-real Element of REAL
(dist ((g /. y),(g /. s))) + (dist ((g /. y),(g /. j))) is V11() real ext-real Element of REAL
Closed-Interval-MSpace (0,1) is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of RealSpace
TopSpaceMetr (Closed-Interval-MSpace (0,1)) is non empty strict TopSpace-like TopStruct
I[01] is non empty strict TopSpace-like T_2 compact V116() SubSpace of R^1
the carrier of I[01] is non empty V181() set
the carrier of (Closed-Interval-MSpace (0,1)) is non empty set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
TOP-REAL n is non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() L15()
the carrier of (TOP-REAL n) is non empty set
K7( the carrier of I[01], the carrier of (TOP-REAL n)) is non empty set
K6(K7( the carrier of I[01], the carrier of (TOP-REAL n))) is non empty set
Euclid n is non empty strict Reflexive discerning V86() triangle Discerning MetrStruct
the carrier of (Euclid n) is non empty set
K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid n)) is non empty set
K6(K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid n))) is non empty set
e is non empty V19() V22( the carrier of I[01]) V23( the carrier of (TOP-REAL n)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL n)) Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL n)))
g is non empty V19() V22( the carrier of (Closed-Interval-MSpace (0,1))) V23( the carrier of (Euclid n)) Function-like total V33( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid n)) Element of K6(K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid n)))
the topology of (TOP-REAL n) is Element of K6(K6( the carrier of (TOP-REAL n)))
K6( the carrier of (TOP-REAL n)) is non empty set
K6(K6( the carrier of (TOP-REAL n))) is non empty set
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is strict TopStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K7( the carrier of I[01], the carrier of (TopSpaceMetr (Euclid n))) is non empty set
K6(K7( the carrier of I[01], the carrier of (TopSpaceMetr (Euclid n)))) is non empty set
p1 is non empty V19() V22( the carrier of I[01]) V23( the carrier of (TopSpaceMetr (Euclid n))) Function-like total V33( the carrier of I[01], the carrier of (TopSpaceMetr (Euclid n))) Element of K6(K7( the carrier of I[01], the carrier of (TopSpaceMetr (Euclid n))))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
TOP-REAL n is non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() L15()
the carrier of (TOP-REAL n) is non empty set
K6( the carrier of (TOP-REAL n)) is non empty set
Euclid n is non empty strict Reflexive discerning V86() triangle Discerning MetrStruct
the carrier of (Euclid n) is non empty set
K6( the carrier of (Euclid n)) is non empty set
e is Element of K6( the carrier of (TOP-REAL n))
(TOP-REAL n) | e is strict SubSpace of TOP-REAL n
the carrier of ((TOP-REAL n) | e) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL n) | e)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL n) | e))) is non empty set
g is non empty Element of K6( the carrier of (Euclid n))
(Euclid n) | g is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of Euclid n
the carrier of ((Euclid n) | g) is non empty set
K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of ((Euclid n) | g)) is non empty set
K6(K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of ((Euclid n) | g))) is non empty set
p1 is V19() V22( the carrier of I[01]) V23( the carrier of ((TOP-REAL n) | e)) Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL n) | e)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL n) | e)))
p2 is non empty V19() V22( the carrier of (Closed-Interval-MSpace (0,1))) V23( the carrier of ((Euclid n) | g)) Function-like total V33( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of ((Euclid n) | g)) Element of K6(K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of ((Euclid n) | g)))
TopSpaceMetr ((Euclid n) | g) is non empty strict TopSpace-like TopStruct
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
TOP-REAL n is non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() L15()
the carrier of (TOP-REAL n) is non empty set
K7( the carrier of I[01], the carrier of (TOP-REAL n)) is non empty set
K6(K7( the carrier of I[01], the carrier of (TOP-REAL n))) is non empty set
e is non empty V19() V22( the carrier of I[01]) V23( the carrier of (TOP-REAL n)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL n)) Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL n)))
Euclid n is non empty strict Reflexive discerning V86() triangle Discerning MetrStruct
the carrier of (Euclid n) is non empty set
K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid n)) is non empty set
K6(K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid n))) is non empty set
n is set
<*n*> is non empty V19() V22( NAT ) Function-like finite V43(1) FinSequence-like FinSubsequence-like set
e is V19() V22( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
e ^ <*n*> is non empty V19() V22( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (e ^ <*n*>) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
len e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
(len e) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
<*n*> ^ e is non empty V19() V22( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len (<*n*> ^ e) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
(e ^ <*n*>) . ((len e) + 1) is set
(<*n*> ^ e) . 1 is set
len <*n*> is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
(len <*n*>) + (len e) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
dom <*n*> is Element of K6(NAT)
<*n*> . 1 is set
n is set
<*n*> is non empty V19() V22( NAT ) Function-like finite V43(1) FinSequence-like FinSubsequence-like set
e is V19() V22( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
e ^ <*n*> is non empty V19() V22( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
(e ^ <*n*>) . 1 is set
e . 1 is set
<*n*> ^ e is non empty V19() V22( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
(len e) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
(<*n*> ^ e) . ((len e) + 1) is set
e . (len e) is set
dom e is Element of K6(NAT)
len <*n*> is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
(len <*n*>) + (len e) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
(<*n*> ^ e) . ((len <*n*>) + (len e)) is set
n is V11() real ext-real set
e is V11() real ext-real set
n - e is V11() real ext-real set
- e is V11() real ext-real set
n + (- e) is V11() real ext-real set
abs (n - e) is V11() real ext-real Element of REAL
e - n is V11() real ext-real set
- n is V11() real ext-real set
e + (- n) is V11() real ext-real set
abs (e - n) is V11() real ext-real Element of REAL
- (e - n) is V11() real ext-real set
- (n - e) is V11() real ext-real set
n is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
[.e,g.] is Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( e <= b₁ & b₁ <= g ) } is set
p1 is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
n - e is V11() real ext-real Element of REAL
- e is V11() real ext-real set
n + (- e) is V11() real ext-real set
abs (n - e) is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
p1 is V11() real ext-real Element of REAL
[.g,p1.] is Element of K6(REAL)
p1 - g is V11() real ext-real Element of REAL
- g is V11() real ext-real set
p1 + (- g) is V11() real ext-real set
e - n is V11() real ext-real Element of REAL
- n is V11() real ext-real set
e + (- n) is V11() real ext-real set
abs (e - n) is V11() real ext-real Element of REAL
n is V19() V22( NAT ) V23( REAL ) Function-like finite FinSequence-like FinSubsequence-like V168() V169() V170() FinSequence of REAL
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
n /. e is V11() real ext-real Element of REAL
dom n is Element of K6(NAT)
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
1 + p1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
e + (1 + p1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
n /. (e + (1 + p1)) is V11() real ext-real Element of REAL
p1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
1 + (p1 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
e + (1 + (p1 + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
n /. (e + (1 + (p1 + 1))) is V11() real ext-real Element of REAL
e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
(e + 1) + p1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
(e + (1 + p1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
g -' (e + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
g - (e + 1) is V11() real ext-real integer Element of REAL
- (e + 1) is V11() real ext-real non positive integer set
g + (- (e + 1)) is V11() real ext-real integer set
1 + (g -' (e + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
e + (1 + (g -' (e + 1))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
n . e is V11() real ext-real set
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
e + (1 + 0) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
n /. (e + (1 + 0)) is V11() real ext-real Element of REAL
n /. g is V11() real ext-real Element of REAL
n . g is V11() real ext-real set
n is V19() V22( NAT ) V23( REAL ) Function-like finite FinSequence-like FinSubsequence-like V168() V169() V170() FinSequence of REAL
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
n /. e is V11() real ext-real Element of REAL
dom n is Element of K6(NAT)
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
1 + p1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
e + (1 + p1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
n /. (e + (1 + p1)) is V11() real ext-real Element of REAL
p1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
1 + (p1 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
e + (1 + (p1 + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
n /. (e + (1 + (p1 + 1))) is V11() real ext-real Element of REAL
e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
(e + 1) + p1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
(e + (1 + p1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
g -' (e + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
g - (e + 1) is V11() real ext-real integer Element of REAL
- (e + 1) is V11() real ext-real non positive integer set
g + (- (e + 1)) is V11() real ext-real integer set
1 + (g -' (e + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
e + (1 + (g -' (e + 1))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
n . e is V11() real ext-real set
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
e + (1 + 0) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
n /. (e + (1 + 0)) is V11() real ext-real Element of REAL
n /. g is V11() real ext-real Element of REAL
n . g is V11() real ext-real set
5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
K6( the carrier of I[01]) is non empty set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
TOP-REAL n is non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() L15()
the carrier of (TOP-REAL n) is non empty set
K7( the carrier of I[01], the carrier of (TOP-REAL n)) is non empty set
K6(K7( the carrier of I[01], the carrier of (TOP-REAL n))) is non empty set
Euclid n is non empty strict Reflexive discerning V86() triangle Discerning MetrStruct
the carrier of (Euclid n) is non empty set
K6( the carrier of (Euclid n)) is non empty set
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
[.0,1.] is Element of K6(REAL)
{1} is non empty set
e is set
[.0,1.] \/ {1} is non empty set
e is V11() real ext-real Element of REAL
g is non empty V19() V22( the carrier of I[01]) V23( the carrier of (TOP-REAL n)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL n)) Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL n)))
e / 2 is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative set
e * (2 ") is V11() real ext-real set
the topology of (TOP-REAL n) is Element of K6(K6( the carrier of (TOP-REAL n)))
K6( the carrier of (TOP-REAL n)) is non empty set
K6(K6( the carrier of (TOP-REAL n))) is non empty set
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is strict TopStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K7( the carrier of I[01], the carrier of (TopSpaceMetr (Euclid n))) is non empty set
K6(K7( the carrier of I[01], the carrier of (TopSpaceMetr (Euclid n)))) is non empty set
K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid n)) is non empty set
K6(K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid n))) is non empty set
h is non empty V19() V22( the carrier of I[01]) V23( the carrier of (TopSpaceMetr (Euclid n))) Function-like total V33( the carrier of I[01], the carrier of (TopSpaceMetr (Euclid n))) Element of K6(K7( the carrier of I[01], the carrier of (TopSpaceMetr (Euclid n))))
dom g is Element of K6( the carrier of I[01])
f is non empty V19() V22( the carrier of (Closed-Interval-MSpace (0,1))) V23( the carrier of (Euclid n)) Function-like total V33( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid n)) Element of K6(K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid n)))
s1 is V11() real ext-real Element of REAL
1 / 2 is V11() real ext-real non negative Element of REAL
1 * (2 ") is V11() real ext-real non negative set
min (s1,(1 / 2)) is V11() real ext-real set
(min (s1,(1 / 2))) / 2 is V11() real ext-real Element of REAL
(min (s1,(1 / 2))) * (2 ") is V11() real ext-real set
2 / (min (s1,(1 / 2))) is V11() real ext-real Element of REAL
(min (s1,(1 / 2))) " is V11() real ext-real set
2 * ((min (s1,(1 / 2))) ") is V11() real ext-real set
[/(2 / (min (s1,(1 / 2))))\] is V11() real ext-real integer set
j is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p is Element of the carrier of (Closed-Interval-MSpace (0,1))
h1 is Element of the carrier of (Closed-Interval-MSpace (0,1))
dist (p,h1) is V11() real ext-real Element of REAL
f /. p is Element of the carrier of (Euclid n)
f . p is Element of the carrier of (Euclid n)
f /. h1 is Element of the carrier of (Euclid n)
f . h1 is Element of the carrier of (Euclid n)
dist ((f /. p),(f /. h1)) is V11() real ext-real Element of REAL
(2 / (min (s1,(1 / 2)))) - j is V11() real ext-real Element of REAL
- j is V11() real ext-real non positive integer set
(2 / (min (s1,(1 / 2)))) + (- j) is V11() real ext-real set
1 + ((2 / (min (s1,(1 / 2)))) - j) is V11() real ext-real Element of REAL
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - j)) is V11() real ext-real Element of REAL
((min (s1,(1 / 2))) / 2) * 1 is V11() real ext-real Element of REAL
Seg j is finite V43(j) Element of K6(NAT)
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
p - 1 is V11() real ext-real integer Element of REAL
- 1 is V11() real ext-real non positive integer set
p + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * (p - 1) is V11() real ext-real Element of REAL
p is V19() V22( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
dom p is Element of K6(NAT)
len p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
Seg (len p) is finite V43( len p) Element of K6(NAT)
<*1*> is non empty V19() V22( NAT ) V23( NAT ) Function-like finite V43(1) FinSequence-like FinSubsequence-like V168() V169() V170() V171() FinSequence of NAT
p ^ <*1*> is non empty V19() V22( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
rng (p ^ <*1*>) is set
h1 is set
len (p ^ <*1*>) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
len <*1*> is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
(len p) + (len <*1*>) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
(len p) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
dom (p ^ <*1*>) is Element of K6(NAT)
y is set
(p ^ <*1*>) . y is set
Seg (len (p ^ <*1*>)) is finite V43( len (p ^ <*1*>)) Element of K6(NAT)
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p . x is set
x - 1 is V11() real ext-real integer Element of REAL
- 1 is V11() real ext-real non positive integer set
x + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * (x - 1) is V11() real ext-real Element of REAL
h1 is V19() V22( NAT ) V23( REAL ) Function-like finite FinSequence-like FinSubsequence-like V168() V169() V170() FinSequence of REAL
len h1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
len <*1*> is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
(len p) + (len <*1*>) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
(len p) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
2 / (1 / 2) is V11() real ext-real non negative Element of REAL
(1 / 2) " is V11() real ext-real non negative set
2 * ((1 / 2) ") is V11() real ext-real non negative set
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
4 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p . y is set
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
p . (y + 1) is set
x is V11() real ext-real Element of REAL
nx is V11() real ext-real Element of REAL
nx - x is V11() real ext-real Element of REAL
- x is V11() real ext-real set
nx + (- x) is V11() real ext-real set
(y + 1) - 1 is V11() real ext-real integer Element of REAL
- 1 is V11() real ext-real non positive integer set
(y + 1) + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * ((y + 1) - 1) is V11() real ext-real Element of REAL
y - 1 is V11() real ext-real integer Element of REAL
y + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * (y - 1) is V11() real ext-real Element of REAL
((min (s1,(1 / 2))) / 2) * y is V11() real ext-real Element of REAL
(((min (s1,(1 / 2))) / 2) * y) - (((min (s1,(1 / 2))) / 2) * (y - 1)) is V11() real ext-real Element of REAL
- (((min (s1,(1 / 2))) / 2) * (y - 1)) is V11() real ext-real set
(((min (s1,(1 / 2))) / 2) * y) + (- (((min (s1,(1 / 2))) / 2) * (y - 1))) is V11() real ext-real set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
p . 1 is set
1 - 1 is V11() real ext-real integer Element of REAL
- 1 is V11() real ext-real non positive integer set
1 + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * (1 - 1) is V11() real ext-real Element of REAL
h1 . 1 is V11() real ext-real set
2 * (min (s1,(1 / 2))) is V11() real ext-real Element of REAL
((min (s1,(1 / 2))) / 2) * (2 / (min (s1,(1 / 2)))) is V11() real ext-real Element of REAL
(2 * (min (s1,(1 / 2)))) / (2 * (min (s1,(1 / 2)))) is V11() real ext-real Element of REAL
(2 * (min (s1,(1 / 2)))) " is V11() real ext-real set
(2 * (min (s1,(1 / 2)))) * ((2 * (min (s1,(1 / 2)))) ") is V11() real ext-real set
j - 1 is V11() real ext-real integer Element of REAL
j + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * (j - 1) is V11() real ext-real Element of REAL
1 - (((min (s1,(1 / 2))) / 2) * (j - 1)) is V11() real ext-real Element of REAL
- (((min (s1,(1 / 2))) / 2) * (j - 1)) is V11() real ext-real set
1 + (- (((min (s1,(1 / 2))) / 2) * (j - 1))) is V11() real ext-real set
(2 / (min (s1,(1 / 2)))) - [/(2 / (min (s1,(1 / 2))))\] is V11() real ext-real Element of REAL
- [/(2 / (min (s1,(1 / 2))))\] is V11() real ext-real integer set
(2 / (min (s1,(1 / 2)))) + (- [/(2 / (min (s1,(1 / 2))))\]) is V11() real ext-real set
1 + ((2 / (min (s1,(1 / 2)))) - [/(2 / (min (s1,(1 / 2))))\]) is V11() real ext-real Element of REAL
((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - [/(2 / (min (s1,(1 / 2))))\])) is V11() real ext-real Element of REAL
p . (len p) is set
y is V11() real ext-real Element of REAL
1 - y is V11() real ext-real Element of REAL
- y is V11() real ext-real set
1 + (- y) is V11() real ext-real set
y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
h1 /. (y + 1) is V11() real ext-real Element of REAL
h1 /. y is V11() real ext-real Element of REAL
(h1 /. (y + 1)) - (h1 /. y) is V11() real ext-real Element of REAL
- (h1 /. y) is V11() real ext-real set
(h1 /. (y + 1)) + (- (h1 /. y)) is V11() real ext-real set
h1 . (y + 1) is V11() real ext-real set
p . (y + 1) is set
h1 . y is V11() real ext-real set
p . y is set
h1 . y is V11() real ext-real set
p . y is set
h1 . (y + 1) is V11() real ext-real set
(2 / (min (s1,(1 / 2)))) + 1 is V11() real ext-real Element of REAL
((2 / (min (s1,(1 / 2)))) + 1) - 1 is V11() real ext-real Element of REAL
((2 / (min (s1,(1 / 2)))) + 1) + (- 1) is V11() real ext-real set
[/(2 / (min (s1,(1 / 2))))\] - 1 is V11() real ext-real integer Element of REAL
[/(2 / (min (s1,(1 / 2))))\] + (- 1) is V11() real ext-real integer set
y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p . y is set
x is V11() real ext-real Element of REAL
y - 1 is V11() real ext-real integer Element of REAL
y + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * (y - 1) is V11() real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
h1 /. (y + 1) is V11() real ext-real Element of REAL
h1 /. y is V11() real ext-real Element of REAL
h1 . (y + 1) is V11() real ext-real set
p . (y + 1) is set
h1 . y is V11() real ext-real set
p . y is set
h1 . y is V11() real ext-real set
p . y is set
h1 . (y + 1) is V11() real ext-real set
y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
h1 /. y is V11() real ext-real Element of REAL
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
h1 /. (y + 1) is V11() real ext-real Element of REAL
[.(h1 /. y),(h1 /. (y + 1)).] is Element of K6(REAL)
x is Element of K6( the carrier of I[01])
g .: x is Element of K6( the carrier of (TOP-REAL n))
nx is Element of K6( the carrier of (Euclid n))
diameter nx is V11() real ext-real Element of REAL
ry is Element of the carrier of (Euclid n)
y is Element of the carrier of (Euclid n)
dist (ry,y) is V11() real ext-real Element of REAL
x3 is set
g . x3 is set
x3 is Element of the carrier of (Closed-Interval-MSpace (0,1))
(h1 /. (y + 1)) - (h1 /. y) is V11() real ext-real Element of REAL
- (h1 /. y) is V11() real ext-real set
(h1 /. (y + 1)) + (- (h1 /. y)) is V11() real ext-real set
y3 is set
g . y3 is set
y3 is Element of the carrier of (Closed-Interval-MSpace (0,1))
f . x3 is Element of the carrier of (Euclid n)
f /. x3 is Element of the carrier of (Euclid n)
f . y3 is Element of the carrier of (Euclid n)
f /. y3 is Element of the carrier of (Euclid n)
r3 is V11() real ext-real Element of REAL
s3 is V11() real ext-real Element of REAL
r3 - s3 is V11() real ext-real Element of REAL
- s3 is V11() real ext-real set
r3 + (- s3) is V11() real ext-real set
abs (r3 - s3) is V11() real ext-real Element of REAL
dist (x3,y3) is V11() real ext-real Element of REAL
rng p is set
y is set
x is set
p . x is set
nx is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p . nx is set
nx - 1 is V11() real ext-real integer Element of REAL
nx + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * (nx - 1) is V11() real ext-real Element of REAL
ry is V11() real ext-real Element of REAL
rng <*1*> is V179() V180() V181() V184() Element of K6(NAT)
rng h1 is V179() V180() V181() Element of K6(REAL)
(rng p) \/ {1} is non empty set
h1 . (len h1) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
TOP-REAL n is non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() L15()
the carrier of (TOP-REAL n) is non empty set
K7( the carrier of I[01], the carrier of (TOP-REAL n)) is non empty set
K6(K7( the carrier of I[01], the carrier of (TOP-REAL n))) is non empty set
Euclid n is non empty strict Reflexive discerning V86() triangle Discerning MetrStruct
the carrier of (Euclid n) is non empty set
K6( the carrier of (Euclid n)) is non empty set
e is V11() real ext-real Element of REAL
g is non empty V19() V22( the carrier of I[01]) V23( the carrier of (TOP-REAL n)) Function-like total V33( the carrier of I[01], the carrier of (TOP-REAL n)) Element of K6(K7( the carrier of I[01], the carrier of (TOP-REAL n)))
dom g is Element of K6( the carrier of I[01])
the topology of (TOP-REAL n) is Element of K6(K6( the carrier of (TOP-REAL n)))
K6( the carrier of (TOP-REAL n)) is non empty set
K6(K6( the carrier of (TOP-REAL n))) is non empty set
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is strict TopStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K7( the carrier of I[01], the carrier of (TopSpaceMetr (Euclid n))) is non empty set
K6(K7( the carrier of I[01], the carrier of (TopSpaceMetr (Euclid n)))) is non empty set
K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid n)) is non empty set
K6(K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid n))) is non empty set
e / 2 is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative set
e * (2 ") is V11() real ext-real set
h is non empty V19() V22( the carrier of I[01]) V23( the carrier of (TopSpaceMetr (Euclid n))) Function-like total V33( the carrier of I[01], the carrier of (TopSpaceMetr (Euclid n))) Element of K6(K7( the carrier of I[01], the carrier of (TopSpaceMetr (Euclid n))))
f is non empty V19() V22( the carrier of (Closed-Interval-MSpace (0,1))) V23( the carrier of (Euclid n)) Function-like total V33( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid n)) Element of K6(K7( the carrier of (Closed-Interval-MSpace (0,1)), the carrier of (Euclid n)))
s1 is V11() real ext-real Element of REAL
1 / 2 is V11() real ext-real non negative Element of REAL
1 * (2 ") is V11() real ext-real non negative set
min (s1,(1 / 2)) is V11() real ext-real set
(min (s1,(1 / 2))) / 2 is V11() real ext-real Element of REAL
(min (s1,(1 / 2))) * (2 ") is V11() real ext-real set
2 / (min (s1,(1 / 2))) is V11() real ext-real Element of REAL
(min (s1,(1 / 2))) " is V11() real ext-real set
2 * ((min (s1,(1 / 2))) ") is V11() real ext-real set
[/(2 / (min (s1,(1 / 2))))\] is V11() real ext-real integer set
j is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p is Element of the carrier of (Closed-Interval-MSpace (0,1))
h1 is Element of the carrier of (Closed-Interval-MSpace (0,1))
dist (p,h1) is V11() real ext-real Element of REAL
f /. p is Element of the carrier of (Euclid n)
f . p is Element of the carrier of (Euclid n)
f /. h1 is Element of the carrier of (Euclid n)
f . h1 is Element of the carrier of (Euclid n)
dist ((f /. p),(f /. h1)) is V11() real ext-real Element of REAL
(2 / (min (s1,(1 / 2)))) - j is V11() real ext-real Element of REAL
- j is V11() real ext-real non positive integer set
(2 / (min (s1,(1 / 2)))) + (- j) is V11() real ext-real set
1 + ((2 / (min (s1,(1 / 2)))) - j) is V11() real ext-real Element of REAL
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - j)) is V11() real ext-real Element of REAL
((min (s1,(1 / 2))) / 2) * 1 is V11() real ext-real Element of REAL
Seg j is finite V43(j) Element of K6(NAT)
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
p - 1 is V11() real ext-real integer Element of REAL
- 1 is V11() real ext-real non positive integer set
p + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * (p - 1) is V11() real ext-real Element of REAL
1 - (((min (s1,(1 / 2))) / 2) * (p - 1)) is V11() real ext-real Element of REAL
- (((min (s1,(1 / 2))) / 2) * (p - 1)) is V11() real ext-real set
1 + (- (((min (s1,(1 / 2))) / 2) * (p - 1))) is V11() real ext-real set
p is V19() V22( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
dom p is Element of K6(NAT)
len p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
Seg (len p) is finite V43( len p) Element of K6(NAT)
<*0*> is non empty V19() V22( NAT ) V23( REAL ) Function-like finite V43(1) FinSequence-like FinSubsequence-like V168() V169() V170() FinSequence of REAL
p ^ <*0*> is non empty V19() V22( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
rng (p ^ <*0*>) is set
h1 is set
len (p ^ <*0*>) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
len <*0*> is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
(len p) + (len <*0*>) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
(len p) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
dom (p ^ <*0*>) is Element of K6(NAT)
y is set
(p ^ <*0*>) . y is set
Seg (len (p ^ <*0*>)) is finite V43( len (p ^ <*0*>)) Element of K6(NAT)
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p . x is set
x - 1 is V11() real ext-real integer Element of REAL
- 1 is V11() real ext-real non positive integer set
x + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * (x - 1) is V11() real ext-real Element of REAL
1 - (((min (s1,(1 / 2))) / 2) * (x - 1)) is V11() real ext-real Element of REAL
- (((min (s1,(1 / 2))) / 2) * (x - 1)) is V11() real ext-real set
1 + (- (((min (s1,(1 / 2))) / 2) * (x - 1))) is V11() real ext-real set
h1 is V19() V22( NAT ) V23( REAL ) Function-like finite FinSequence-like FinSubsequence-like V168() V169() V170() FinSequence of REAL
len h1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
len <*0*> is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
(len p) + (len <*0*>) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
(len p) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
2 / (1 / 2) is V11() real ext-real non negative Element of REAL
(1 / 2) " is V11() real ext-real non negative set
2 * ((1 / 2) ") is V11() real ext-real non negative set
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
4 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p . y is set
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
p . (y + 1) is set
x is V11() real ext-real Element of REAL
nx is V11() real ext-real Element of REAL
x - nx is V11() real ext-real Element of REAL
- nx is V11() real ext-real set
x + (- nx) is V11() real ext-real set
y - 1 is V11() real ext-real integer Element of REAL
- 1 is V11() real ext-real non positive integer set
y + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * (y - 1) is V11() real ext-real Element of REAL
1 - (((min (s1,(1 / 2))) / 2) * (y - 1)) is V11() real ext-real Element of REAL
- (((min (s1,(1 / 2))) / 2) * (y - 1)) is V11() real ext-real set
1 + (- (((min (s1,(1 / 2))) / 2) * (y - 1))) is V11() real ext-real set
(y + 1) - 1 is V11() real ext-real integer Element of REAL
(y + 1) + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * ((y + 1) - 1) is V11() real ext-real Element of REAL
1 - (((min (s1,(1 / 2))) / 2) * ((y + 1) - 1)) is V11() real ext-real Element of REAL
- (((min (s1,(1 / 2))) / 2) * ((y + 1) - 1)) is V11() real ext-real set
1 + (- (((min (s1,(1 / 2))) / 2) * ((y + 1) - 1))) is V11() real ext-real set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
p . 1 is set
1 - 1 is V11() real ext-real integer Element of REAL
- 1 is V11() real ext-real non positive integer set
1 + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * (1 - 1) is V11() real ext-real Element of REAL
1 - (((min (s1,(1 / 2))) / 2) * (1 - 1)) is V11() real ext-real Element of REAL
- (((min (s1,(1 / 2))) / 2) * (1 - 1)) is V11() real ext-real set
1 + (- (((min (s1,(1 / 2))) / 2) * (1 - 1))) is V11() real ext-real set
h1 . 1 is V11() real ext-real set
2 * (min (s1,(1 / 2))) is V11() real ext-real Element of REAL
((min (s1,(1 / 2))) / 2) * (2 / (min (s1,(1 / 2)))) is V11() real ext-real Element of REAL
(2 * (min (s1,(1 / 2)))) / (2 * (min (s1,(1 / 2)))) is V11() real ext-real Element of REAL
(2 * (min (s1,(1 / 2)))) " is V11() real ext-real set
(2 * (min (s1,(1 / 2)))) * ((2 * (min (s1,(1 / 2)))) ") is V11() real ext-real set
j - 1 is V11() real ext-real integer Element of REAL
j + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * (j - 1) is V11() real ext-real Element of REAL
1 - (((min (s1,(1 / 2))) / 2) * (j - 1)) is V11() real ext-real Element of REAL
- (((min (s1,(1 / 2))) / 2) * (j - 1)) is V11() real ext-real set
1 + (- (((min (s1,(1 / 2))) / 2) * (j - 1))) is V11() real ext-real set
(2 / (min (s1,(1 / 2)))) - [/(2 / (min (s1,(1 / 2))))\] is V11() real ext-real Element of REAL
- [/(2 / (min (s1,(1 / 2))))\] is V11() real ext-real integer set
(2 / (min (s1,(1 / 2)))) + (- [/(2 / (min (s1,(1 / 2))))\]) is V11() real ext-real set
1 + ((2 / (min (s1,(1 / 2)))) - [/(2 / (min (s1,(1 / 2))))\]) is V11() real ext-real Element of REAL
((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - [/(2 / (min (s1,(1 / 2))))\])) is V11() real ext-real Element of REAL
p . (len p) is set
y is V11() real ext-real Element of REAL
y - 0 is V11() real ext-real Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered set
y + (- 0) is V11() real ext-real set
(len p) - 1 is V11() real ext-real integer Element of REAL
(len p) + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * ((len p) - 1) is V11() real ext-real Element of REAL
1 - (((min (s1,(1 / 2))) / 2) * ((len p) - 1)) is V11() real ext-real Element of REAL
- (((min (s1,(1 / 2))) / 2) * ((len p) - 1)) is V11() real ext-real set
1 + (- (((min (s1,(1 / 2))) / 2) * ((len p) - 1))) is V11() real ext-real set
y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
h1 /. y is V11() real ext-real Element of REAL
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
h1 /. (y + 1) is V11() real ext-real Element of REAL
(h1 /. y) - (h1 /. (y + 1)) is V11() real ext-real Element of REAL
- (h1 /. (y + 1)) is V11() real ext-real set
(h1 /. y) + (- (h1 /. (y + 1))) is V11() real ext-real set
h1 . (y + 1) is V11() real ext-real set
p . (y + 1) is set
h1 . y is V11() real ext-real set
p . y is set
h1 . y is V11() real ext-real set
p . y is set
h1 . (y + 1) is V11() real ext-real set
(2 / (min (s1,(1 / 2)))) + 1 is V11() real ext-real Element of REAL
((2 / (min (s1,(1 / 2)))) + 1) - 1 is V11() real ext-real Element of REAL
((2 / (min (s1,(1 / 2)))) + 1) + (- 1) is V11() real ext-real set
[/(2 / (min (s1,(1 / 2))))\] - 1 is V11() real ext-real integer Element of REAL
[/(2 / (min (s1,(1 / 2))))\] + (- 1) is V11() real ext-real integer set
y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p . y is set
x is V11() real ext-real Element of REAL
y - 1 is V11() real ext-real integer Element of REAL
y + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * (y - 1) is V11() real ext-real Element of REAL
1 - (((min (s1,(1 / 2))) / 2) * (y - 1)) is V11() real ext-real Element of REAL
- (((min (s1,(1 / 2))) / 2) * (y - 1)) is V11() real ext-real set
1 + (- (((min (s1,(1 / 2))) / 2) * (y - 1))) is V11() real ext-real set
y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
h1 /. y is V11() real ext-real Element of REAL
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
h1 /. (y + 1) is V11() real ext-real Element of REAL
h1 . (y + 1) is V11() real ext-real set
p . (y + 1) is set
h1 . y is V11() real ext-real set
p . y is set
h1 . y is V11() real ext-real set
p . y is set
h1 . (y + 1) is V11() real ext-real set
y is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer Element of NAT
h1 /. (y + 1) is V11() real ext-real Element of REAL
h1 /. y is V11() real ext-real Element of REAL
[.(h1 /. (y + 1)),(h1 /. y).] is Element of K6(REAL)
x is Element of K6( the carrier of I[01])
g .: x is Element of K6( the carrier of (TOP-REAL n))
nx is Element of K6( the carrier of (Euclid n))
diameter nx is V11() real ext-real Element of REAL
ry is Element of the carrier of (Euclid n)
y is Element of the carrier of (Euclid n)
dist (ry,y) is V11() real ext-real Element of REAL
x3 is set
g . x3 is set
x3 is Element of the carrier of (Closed-Interval-MSpace (0,1))
f /. x3 is Element of the carrier of (Euclid n)
f . x3 is Element of the carrier of (Euclid n)
y3 is set
g . y3 is set
y3 is Element of the carrier of (Closed-Interval-MSpace (0,1))
(h1 /. y) - (h1 /. (y + 1)) is V11() real ext-real Element of REAL
- (h1 /. (y + 1)) is V11() real ext-real set
(h1 /. y) + (- (h1 /. (y + 1))) is V11() real ext-real set
r3 is V11() real ext-real Element of REAL
s3 is V11() real ext-real Element of REAL
r3 - s3 is V11() real ext-real Element of REAL
- s3 is V11() real ext-real set
r3 + (- s3) is V11() real ext-real set
abs (r3 - s3) is V11() real ext-real Element of REAL
dist (x3,y3) is V11() real ext-real Element of REAL
f . y3 is Element of the carrier of (Euclid n)
f /. y3 is Element of the carrier of (Euclid n)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
[.0,1.] is Element of K6(REAL)
{0} is non empty set
y is set
[.0,1.] \/ {0} is non empty set
rng p is set
y is set
x is set
p . x is set
nx is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT
p . nx is set
nx - 1 is V11() real ext-real integer Element of REAL
nx + (- 1) is V11() real ext-real integer set
((min (s1,(1 / 2))) / 2) * (nx - 1) is V11() real ext-real Element of REAL
1 - (((min (s1,(1 / 2))) / 2) * (nx - 1)) is V11() real ext-real Element of REAL
- (((min (s1,(1 / 2))) / 2) * (nx - 1)) is V11() real ext-real set
1 + (- (((min (s1,(1 / 2))) / 2) * (nx - 1))) is V11() real ext-real set
1 - 0 is non empty V11() real ext-real positive non negative integer Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered set
1 + (- 0) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer set
ry is V11() real ext-real Element of REAL
rng <*0*> is V179() V180() V181() Element of K6(REAL)
rng h1 is V179() V180() V181() Element of K6(REAL)
(rng p) \/ {0} is non empty set
h1 . (len h1) is V11() real ext-real set