:: 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

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT

{ b

( f <= b

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

( ry <= b

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

( x3 <= b

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

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

( b

for b

( not b

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

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

[.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