:: UNIFORM1 semantic presentation

REAL is non empty non finite set

K6(REAL) is non empty set

K6(NAT) is non empty set

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

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

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 () is non empty set
K298( the carrier of ()) is non empty functional FinSequence-membered M16( the carrier of ())

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

the carrier of () is non empty set
K7( the carrier of n, the carrier of ()) is non empty set
K6(K7( the carrier of n, the carrier of ())) is non empty set
the carrier of e is non empty set
K6( the carrier of ()) is non empty set
g is non empty V19() V22( the carrier of n) V23( the carrier of ()) Function-like total V33( the carrier of n, the carrier of ()) Element of K6(K7( the carrier of n, the carrier of ()))
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 ())
g " h is Element of K6( the carrier of n)
K6( the carrier of n) is non empty set
[#] () is non empty non proper Element of K6( the carrier of ())
f is Element of K6( the carrier of ())

the carrier of () is non empty set

the carrier of () is non empty set
K7( the carrier of (), the carrier of ()) is non empty set
K6(K7( the carrier of (), the carrier of ())) 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 ()) V23( the carrier of ()) Function-like total V33( the carrier of (), the carrier of ()) Element of K6(K7( the carrier of (), the carrier of ()))
dom g is Element of K6( the carrier of ())
K6( the carrier of ()) is non empty set
K6( the carrier of ()) 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 ())
g " h is Element of K6( the carrier of ())
s1 is Element of the carrier of n
g . s1 is set
f is Element of K6( the carrier of ())
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 ())
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

the carrier of () is non empty set

the carrier of () is non empty set
K7( the carrier of (), the carrier of ()) is non empty set
K6(K7( the carrier of (), the carrier of ())) 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 ()) V23( the carrier of ()) Function-like total V33( the carrier of (), the carrier of ()) Element of K6(K7( the carrier of (), the carrier of ()))
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 ()) 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 ())
K6( the carrier of ()) is non empty set
f is Element of K6( the carrier of ())
g " f is Element of K6( the carrier of ())
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)

the carrier of n is non empty set

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

the carrier of () is non empty set

the carrier of () is non empty set
K7( the carrier of (), the carrier of ()) is non empty set
K6(K7( the carrier of (), the carrier of ())) 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 ()) V23( the carrier of ()) Function-like total V33( the carrier of (), the carrier of ()) Element of K6(K7( the carrier of (), the carrier of ()))
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

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
K6(K6( the carrier of ())) is non empty set
the carrier of n is non empty set
e is Element of K6(K6( the carrier of ()))
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,() #) is strict TopStruct
p1 is set

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

j is Element of the carrier of n

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 ()))
{ b1 where b1 is Element of the carrier of n : S3[b1] } is set

{ b1 where b1 is Element of the carrier of n : ex b2 being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT st
( f <= b2 & b1 = p1 . b2 )
}
is set

p1 . f is Element of the carrier of n
s1 is Element of K6(K6( the carrier of ()))
clf s1 is Element of K6(K6( the carrier of ()))
f is Element of K6( the carrier of ())
Cl f is Element of K6( the carrier of ())
j is set
meet j is set
p is Element of K6(K6( the carrier of ()))
h1 is set
y is set
x is Element of K6( the carrier of ())
nx is Element of K6( the carrier of ())
Cl nx is Element of K6( the carrier of ())

{ b1 where b1 is Element of the carrier of n : ex b2 being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT st
( ry <= b2 & b1 = p1 . b2 )
}
is set

y is Element of K6( the carrier of ())
x3 is Element of K6( the carrier of ())
Cl x3 is Element of K6( the carrier of ())

{ b1 where b1 is Element of the carrier of n : ex b2 being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer Element of NAT st
( x3 <= b2 & b1 = p1 . b2 )
}
is set

r3 is set
y3 is Element of the carrier of n

p1 . y3 is Element of the carrier of n

p1 . y3 is Element of the carrier of n
r3 is set
y3 is Element of the carrier of n

p1 . y3 is Element of the carrier of n

p1 . y3 is Element of the carrier of n
h1 is set
meet p is Element of K6( the carrier of ())
y is Element of K6( the carrier of ())
x is Element of K6( the carrier of ())
Cl x is Element of K6( the carrier of ())
meet (clf s1) is Element of K6( the carrier of ())
j is Element of the carrier of ()
p is Element of the carrier of n
h1 is Element of K6( the carrier of ())
y is Element of K6( the carrier of ())
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

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 ())
{ b1 where b1 is Element of the carrier of () : S4[b1] } is set
x3 is Element of K6( the carrier of ())
Cl x3 is Element of K6( the carrier of ())
x3 is set
r3 is Element of the carrier of n
dist (p,r3) is V11() real ext-real Element of REAL

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

p1 . y3 is Element of the carrier of n

p1 . y3 is Element of the carrier of n

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

the carrier of n is non empty set

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

the carrier of () is non empty set

the carrier of () is non empty set
K7( the carrier of (), the carrier of ()) is non empty set
K6(K7( the carrier of (), the carrier of ())) 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 ()) V23( the carrier of ()) Function-like total V33( the carrier of (), the carrier of ()) Element of K6(K7( the carrier of (), the carrier of ()))
p2 is V11() real ext-real Element of REAL
K6( the carrier of ()) 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
{ b1 where b1 is Element of K6( the carrier of ()) : ex b2 being Element of the carrier of n ex b3 being V11() real ext-real Element of REAL st
( b1 = Ball (b2,b3) & ( for b4 being Element of the carrier of n
for b5, b6 being Element of the carrier of e holds
( not b5 = g . b2 or not b6 = g . b4 or b3 <= dist (b2,b4) or not p2 / 2 <= dist (b5,b6) ) ) )
}
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 ())
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 ())) is non empty set
f is Element of K6(K6( the carrier of ()))
s1 is Element of K6( the carrier of ())
s is Element of K6( the carrier of ())
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 ())
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 ())
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 ())
h1 is Element of K6( the carrier of ())
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

the carrier of I[01] is non empty V181() set
the carrier of () is non empty set

TOP-REAL n is non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() L15()
the carrier of () is non empty set
K7( the carrier of I[01], the carrier of ()) is non empty set
K6(K7( the carrier of I[01], the carrier of ())) is non empty set

the carrier of () is non empty set
K7( the carrier of (), the carrier of ()) is non empty set
K6(K7( the carrier of (), the carrier of ())) is non empty set
e is non empty V19() V22( the carrier of I[01]) V23( the carrier of ()) Function-like total V33( the carrier of I[01], the carrier of ()) Element of K6(K7( the carrier of I[01], the carrier of ()))
g is non empty V19() V22( the carrier of ()) V23( the carrier of ()) Function-like total V33( the carrier of (), the carrier of ()) Element of K6(K7( the carrier of (), the carrier of ()))
the topology of () is Element of K6(K6( the carrier of ()))
K6( the carrier of ()) is non empty set
K6(K6( the carrier of ())) is non empty set
TopStruct(# the carrier of (), the topology of () #) is strict TopStruct

the carrier of () is non empty set
K7( the carrier of I[01], the carrier of ()) is non empty set
K6(K7( the carrier of I[01], the carrier of ())) is non empty set
p1 is non empty V19() V22( the carrier of I[01]) V23( the carrier of ()) Function-like total V33( the carrier of I[01], the carrier of ()) Element of K6(K7( the carrier of I[01], the carrier of ()))

TOP-REAL n is non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() L15()
the carrier of () is non empty set
K6( the carrier of ()) is non empty set

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
e is Element of K6( the carrier of ())
() | e is strict SubSpace of TOP-REAL n
the carrier of (() | e) is set
K7( the carrier of I[01], the carrier of (() | e)) is set
K6(K7( the carrier of I[01], the carrier of (() | e))) is non empty set
g is non empty Element of K6( the carrier of ())
() | g is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of Euclid n
the carrier of (() | g) is non empty set
K7( the carrier of (), the carrier of (() | g)) is non empty set
K6(K7( the carrier of (), the carrier of (() | g))) is non empty set
p1 is V19() V22( the carrier of I[01]) V23( the carrier of (() | e)) Function-like V33( the carrier of I[01], the carrier of (() | e)) Element of K6(K7( the carrier of I[01], the carrier of (() | e)))
p2 is non empty V19() V22( the carrier of ()) V23( the carrier of (() | g)) Function-like total V33( the carrier of (), the carrier of (() | g)) Element of K6(K7( the carrier of (), the carrier of (() | g)))
TopSpaceMetr (() | g) is non empty strict TopSpace-like TopStruct

TOP-REAL n is non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() L15()
the carrier of () is non empty set
K7( the carrier of I[01], the carrier of ()) is non empty set
K6(K7( the carrier of I[01], the carrier of ())) is non empty set
e is non empty V19() V22( the carrier of I[01]) V23( the carrier of ()) Function-like total V33( the carrier of I[01], the carrier of ()) Element of K6(K7( the carrier of I[01], the carrier of ()))

the carrier of () is non empty set
K7( the carrier of (), the carrier of ()) is non empty set
K6(K7( the carrier of (), the carrier of ())) is non empty set
n is set

(e ^ <*n*>) . ((len e) + 1) is set
(<*n*> ^ e) . 1 is set

dom <*n*> is Element of K6(NAT)
<*n*> . 1 is set
n is set

(e ^ <*n*>) . 1 is set
e . 1 is set

(<*n*> ^ e) . ((len e) + 1) is set
e . (len e) is set
dom e is Element of K6(NAT)

(<*n*> ^ e) . (() + (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)
{ b1 where b1 is V11() real ext-real Element of REAL : ( e <= b1 & b1 <= 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 /. e is V11() real ext-real Element of REAL
dom n is Element of K6(NAT)

n /. (e + (1 + p1)) is V11() real ext-real Element of REAL

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 + p1)) + 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 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

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 /. e is V11() real ext-real Element of REAL
dom n is Element of K6(NAT)

n /. (e + (1 + p1)) is V11() real ext-real Element of REAL

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 + p1)) + 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 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

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

K6( the carrier of I[01]) is non empty set

TOP-REAL n is non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() L15()
the carrier of () is non empty set
K7( the carrier of I[01], the carrier of ()) is non empty set
K6(K7( the carrier of I[01], the carrier of ())) is non empty set

the carrier of () is non empty set
K6( the carrier of ()) is non empty set
{ b1 where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 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 ()) Function-like total V33( the carrier of I[01], the carrier of ()) Element of K6(K7( the carrier of I[01], the carrier of ()))
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 () is Element of K6(K6( the carrier of ()))
K6( the carrier of ()) is non empty set
K6(K6( the carrier of ())) is non empty set
TopStruct(# the carrier of (), the topology of () #) is strict TopStruct

the carrier of () is non empty set
K7( the carrier of I[01], the carrier of ()) is non empty set
K6(K7( the carrier of I[01], the carrier of ())) is non empty set
K7( the carrier of (), the carrier of ()) is non empty set
K6(K7( the carrier of (), the carrier of ())) is non empty set
h is non empty V19() V22( the carrier of I[01]) V23( the carrier of ()) Function-like total V33( the carrier of I[01], the carrier of ()) Element of K6(K7( the carrier of I[01], the carrier of ()))
dom g is Element of K6( the carrier of I[01])
f is non empty V19() V22( the carrier of ()) V23( the carrier of ()) Function-like total V33( the carrier of (), the carrier of ()) Element of K6(K7( the carrier of (), the carrier of ()))
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

p is Element of the carrier of ()
h1 is Element of the carrier of ()
dist (p,h1) is V11() real ext-real Element of REAL
f /. p is Element of the carrier of ()
f . p is Element of the carrier of ()
f /. h1 is Element of the carrier of ()
f . h1 is Element of the carrier of ()
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

(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

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

dom p is Element of K6(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

rng (p ^ <*1*>) is set
h1 is set

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)

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

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

p . y is set

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

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

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

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

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

h1 /. y is V11() real ext-real Element of REAL

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 ())
nx is Element of K6( the carrier of ())

ry is Element of the carrier of ()
y is Element of the carrier of ()
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 ()
(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 ()
f . x3 is Element of the carrier of ()
f /. x3 is Element of the carrier of ()
f . y3 is Element of the carrier of ()
f /. y3 is Element of the carrier of ()
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

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

TOP-REAL n is non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() L15()
the carrier of () is non empty set
K7( the carrier of I[01], the carrier of ()) is non empty set
K6(K7( the carrier of I[01], the carrier of ())) is non empty set

the carrier of () is non empty set
K6( the carrier of ()) 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 ()) Function-like total V33( the carrier of I[01], the carrier of ()) Element of K6(K7( the carrier of I[01], the carrier of ()))
dom g is Element of K6( the carrier of I[01])
the topology of () is Element of K6(K6( the carrier of ()))
K6( the carrier of ()) is non empty set
K6(K6( the carrier of ())) is non empty set
TopStruct(# the carrier of (), the topology of () #) is strict TopStruct

the carrier of () is non empty set
K7( the carrier of I[01], the carrier of ()) is non empty set
K6(K7( the carrier of I[01], the carrier of ())) is non empty set
K7( the carrier of (), the carrier of ()) is non empty set
K6(K7( the carrier of (), the carrier of ())) 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 ()) Function-like total V33( the carrier of I[01], the carrier of ()) Element of K6(K7( the carrier of I[01], the carrier of ()))
f is non empty V19() V22( the carrier of ()) V23( the carrier of ()) Function-like total V33( the carrier of (), the carrier of ()) Element of K6(K7( the carrier of (), the carrier of ()))
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

p is Element of the carrier of ()
h1 is Element of the carrier of ()
dist (p,h1) is V11() real ext-real Element of REAL
f /. p is Element of the carrier of ()
f . p is Element of the carrier of ()
f /. h1 is Element of the carrier of ()
f . h1 is Element of the carrier of ()
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

(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

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

dom p is Element of K6(NAT)

Seg (len p) is finite V43( len p) Element of K6(NAT)

rng () is set
h1 is set

dom () is Element of K6(NAT)
y is set
() . y is set
Seg (len ()) is finite V43( len ()) Element of K6(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

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

p . y is set

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

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

y + () 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

h1 /. y is V11() real ext-real Element of REAL

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

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