:: BHSP_2 semantic presentation

REAL is V127() V128() V129() V133() set

NAT is V4() epsilon-transitive epsilon-connected ordinal V127() V128() V129() V130() V131() V132() V133() Element of K32(REAL)

K32(REAL) is set

COMPLEX is V127() V133() set

omega is V4() epsilon-transitive epsilon-connected ordinal V127() V128() V129() V130() V131() V132() V133() set

K32(omega) is set

K32(NAT) is set

K33(NAT,REAL) is set

K32(K33(NAT,REAL)) is set

RAT is V127() V128() V129() V130() V133() set

INT is V127() V128() V129() V130() V131() V133() set

0 is V4() ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real V127() V128() V129() V130() V131() V132() V133() set

1 is V4() ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

0 is V4() ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() V133() Element of NAT

- 1 is ext-real non positive V27() real Element of REAL

2 is V4() ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

r is Element of the carrier of X

y is Element of the carrier of X

q is ext-real V27() real Element of REAL

k is V4() ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() V133() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

x . n is Element of the carrier of X

dist ((x . n),y) is ext-real V27() real Element of REAL

dist (r,y) is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

y is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

y is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

q is Element of the carrier of X

k is Element of the carrier of X

n is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

x . k is Element of the carrier of X

dist ((x . k),q) is ext-real V27() real Element of REAL

r . k is Element of the carrier of X

dist ((r . k),k) is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . k is Element of the carrier of X

x . k is Element of the carrier of X

dist ((r . k),k) is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

x + r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

y is Element of the carrier of X

q is Element of the carrier of X

y + q is Element of the carrier of X

k is Element of the carrier of X

n is ext-real V27() real Element of REAL

n / 2 is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n + n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(x + r) . n is Element of the carrier of X

dist (((x + r) . n),k) is ext-real V27() real Element of REAL

r . n is Element of the carrier of X

dist ((r . n),q) is ext-real V27() real Element of REAL

x . n is Element of the carrier of X

(x . n) + (r . n) is Element of the carrier of X

dist (((x . n) + (r . n)),(y + q)) is ext-real V27() real Element of REAL

dist ((x . n),y) is ext-real V27() real Element of REAL

(dist ((x . n),y)) + (dist ((r . n),q)) is ext-real V27() real Element of REAL

(n / 2) + (n / 2) is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

x - r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

y is Element of the carrier of X

q is Element of the carrier of X

y - q is Element of the carrier of X

k is Element of the carrier of X

n is ext-real V27() real Element of REAL

n / 2 is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n + n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(x - r) . n is Element of the carrier of X

dist (((x - r) . n),k) is ext-real V27() real Element of REAL

r . n is Element of the carrier of X

dist ((r . n),q) is ext-real V27() real Element of REAL

x . n is Element of the carrier of X

(x . n) - (r . n) is Element of the carrier of X

dist (((x . n) - (r . n)),(y - q)) is ext-real V27() real Element of REAL

dist ((x . n),y) is ext-real V27() real Element of REAL

(dist ((x . n),y)) + (dist ((r . n),q)) is ext-real V27() real Element of REAL

(n / 2) + (n / 2) is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is ext-real V27() real Element of REAL

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

x * r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

y is Element of the carrier of X

x * y is Element of the carrier of X

q is Element of the carrier of X

abs x is ext-real V27() real Element of REAL

0 / (abs x) is ext-real V27() real Element of REAL

k is ext-real V27() real Element of REAL

k / (abs x) is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . n is Element of the carrier of X

dist ((r . n),y) is ext-real V27() real Element of REAL

(abs x) * (k / (abs x)) is ext-real V27() real Element of REAL

(abs x) " is ext-real V27() real Element of REAL

((abs x) ") * k is ext-real V27() real Element of REAL

(abs x) * (((abs x) ") * k) is ext-real V27() real Element of REAL

(abs x) * ((abs x) ") is ext-real V27() real Element of REAL

((abs x) * ((abs x) ")) * k is ext-real V27() real Element of REAL

1 * k is ext-real V27() real Element of REAL

x * (r . n) is Element of the carrier of X

dist ((x * (r . n)),(x * y)) is ext-real V27() real Element of REAL

(x * (r . n)) - (x * y) is Element of the carrier of X

||.((x * (r . n)) - (x * y)).|| is ext-real V27() real Element of REAL

(r . n) - y is Element of the carrier of X

x * ((r . n) - y) is Element of the carrier of X

||.(x * ((r . n) - y)).|| is ext-real V27() real Element of REAL

||.((r . n) - y).|| is ext-real V27() real Element of REAL

(abs x) * ||.((r . n) - y).|| is ext-real V27() real Element of REAL

(abs x) * (dist ((r . n),y)) is ext-real V27() real Element of REAL

dist ((x * (r . n)),q) is ext-real V27() real Element of REAL

(x * r) . n is Element of the carrier of X

dist (((x * r) . n),q) is ext-real V27() real Element of REAL

k is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . n is Element of the carrier of X

dist ((r . n),y) is ext-real V27() real Element of REAL

x * (r . n) is Element of the carrier of X

dist ((x * (r . n)),(x * y)) is ext-real V27() real Element of REAL

0 * (r . n) is Element of the carrier of X

0. X is V64(X) Element of the carrier of X

dist ((0 * (r . n)),H

dist (H

dist ((x * (r . n)),q) is ext-real V27() real Element of REAL

(x * r) . n is Element of the carrier of X

dist (((x * r) . n),q) is ext-real V27() real Element of REAL

k is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

- x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(- 1) * x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

r + x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

y is Element of the carrier of X

y + x is Element of the carrier of X

q is ext-real V27() real Element of REAL

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(r + x) . n is Element of the carrier of X

dist (((r + x) . n),(y + x)) is ext-real V27() real Element of REAL

r . n is Element of the carrier of X

(r . n) + x is Element of the carrier of X

dist (((r . n) + x),(y + x)) is ext-real V27() real Element of REAL

dist ((r . n),y) is ext-real V27() real Element of REAL

dist (x,x) is ext-real V27() real Element of REAL

(dist ((r . n),y)) + (dist (x,x)) is ext-real V27() real Element of REAL

(dist ((r . n),y)) + 0 is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

r - x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

- x is Element of the carrier of X

r + (- x) is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

r is Element of the carrier of X

y is ext-real V27() real Element of REAL

q is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

x . n is Element of the carrier of X

(x . n) - r is Element of the carrier of X

||.((x . n) - r).|| is ext-real V27() real Element of REAL

dist ((x . n),r) is ext-real V27() real Element of REAL

r is Element of the carrier of X

y is ext-real V27() real Element of REAL

q is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

x . n is Element of the carrier of X

dist ((x . n),r) is ext-real V27() real Element of REAL

(x . n) - r is Element of the carrier of X

||.((x . n) - r).|| is ext-real V27() real Element of REAL

r is Element of the carrier of X

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

r is Element of the carrier of X

y is Element of the carrier of X

dist (r,y) is ext-real V27() real Element of REAL

4 is V4() ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(dist (r,y)) / 4 is ext-real V27() real Element of REAL

0 / 4 is V4() ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real V127() V128() V129() V130() V131() V132() V133() Element of REAL

q is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

x . q is Element of the carrier of X

dist ((x . q),y) is ext-real V27() real Element of REAL

r - (x . q) is Element of the carrier of X

y - (x . q) is Element of the carrier of X

dist ((r - (x . q)),(y - (x . q))) is ext-real V27() real Element of REAL

dist ((x . q),r) is ext-real V27() real Element of REAL

(dist ((x . q),r)) + (dist ((x . q),y)) is ext-real V27() real Element of REAL

((dist (r,y)) / 4) + ((dist (r,y)) / 4) is ext-real V27() real Element of REAL

(dist (r,y)) / 2 is ext-real V27() real Element of REAL

x . k is Element of the carrier of X

dist ((x . k),r) is ext-real V27() real Element of REAL

r - (x . k) is Element of the carrier of X

y - (x . k) is Element of the carrier of X

dist ((r - (x . k)),(y - (x . k))) is ext-real V27() real Element of REAL

dist ((x . k),y) is ext-real V27() real Element of REAL

(dist ((x . k),r)) + (dist ((x . k),y)) is ext-real V27() real Element of REAL

r is Element of the carrier of X

y is Element of the carrier of X

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

rng r is set

(X,r) is Element of the carrier of X

y is Element of the carrier of X

{y} is V4() set

q is Element of the carrier of X

k is ext-real V27() real Element of REAL

n is V4() ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() V133() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

dom r is set

r . n is Element of the carrier of X

dist ((r . n),x) is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,r) is Element of the carrier of X

y is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . y is Element of the carrier of X

y is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . y is Element of the carrier of X

dom r is set

rng r is set

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,x) is Element of the carrier of X

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,r) is Element of the carrier of X

y is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

y is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

q is ext-real V27() real Element of REAL

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

x . n is Element of the carrier of X

dist ((x . n),(X,x)) is ext-real V27() real Element of REAL

r . n is Element of the carrier of X

dist ((r . n),(X,x)) is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . n is Element of the carrier of X

x . n is Element of the carrier of X

dist ((r . n),(X,x)) is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

q is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,x) is Element of the carrier of X

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

x + r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,(x + r)) is Element of the carrier of X

(X,r) is Element of the carrier of X

(X,x) + (X,r) is Element of the carrier of X

n is ext-real V27() real Element of REAL

n / 2 is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n + n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . n is Element of the carrier of X

dist ((r . n),(X,r)) is ext-real V27() real Element of REAL

(x + r) . n is Element of the carrier of X

dist (((x + r) . n),((X,x) + (X,r))) is ext-real V27() real Element of REAL

x . n is Element of the carrier of X

(x . n) + (r . n) is Element of the carrier of X

dist (((x . n) + (r . n)),((X,x) + (X,r))) is ext-real V27() real Element of REAL

dist ((x . n),(X,x)) is ext-real V27() real Element of REAL

(dist ((x . n),(X,x))) + (dist ((r . n),(X,r))) is ext-real V27() real Element of REAL

(n / 2) + (n / 2) is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,x) is Element of the carrier of X

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

x - r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,(x - r)) is Element of the carrier of X

(X,r) is Element of the carrier of X

(X,x) - (X,r) is Element of the carrier of X

n is ext-real V27() real Element of REAL

n / 2 is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n + n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . n is Element of the carrier of X

dist ((r . n),(X,r)) is ext-real V27() real Element of REAL

(x - r) . n is Element of the carrier of X

dist (((x - r) . n),((X,x) - (X,r))) is ext-real V27() real Element of REAL

x . n is Element of the carrier of X

(x . n) - (r . n) is Element of the carrier of X

dist (((x . n) - (r . n)),((X,x) - (X,r))) is ext-real V27() real Element of REAL

dist ((x . n),(X,x)) is ext-real V27() real Element of REAL

(dist ((x . n),(X,x))) + (dist ((r . n),(X,r))) is ext-real V27() real Element of REAL

(n / 2) + (n / 2) is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is ext-real V27() real Element of REAL

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

x * r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,(x * r)) is Element of the carrier of X

(X,r) is Element of the carrier of X

x * (X,r) is Element of the carrier of X

k is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . n is Element of the carrier of X

dist ((r . n),(X,r)) is ext-real V27() real Element of REAL

x * (r . n) is Element of the carrier of X

dist ((x * (r . n)),(x * (X,r))) is ext-real V27() real Element of REAL

0 * (r . n) is Element of the carrier of X

0. X is V64(X) Element of the carrier of X

dist ((0 * (r . n)),H

dist (H

(x * r) . n is Element of the carrier of X

dist (((x * r) . n),(x * (X,r))) is ext-real V27() real Element of REAL

abs x is ext-real V27() real Element of REAL

0 / (abs x) is ext-real V27() real Element of REAL

k is ext-real V27() real Element of REAL

k / (abs x) is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . n is Element of the carrier of X

dist ((r . n),(X,r)) is ext-real V27() real Element of REAL

(abs x) * (k / (abs x)) is ext-real V27() real Element of REAL

(abs x) " is ext-real V27() real Element of REAL

((abs x) ") * k is ext-real V27() real Element of REAL

(abs x) * (((abs x) ") * k) is ext-real V27() real Element of REAL

(abs x) * ((abs x) ") is ext-real V27() real Element of REAL

((abs x) * ((abs x) ")) * k is ext-real V27() real Element of REAL

1 * k is ext-real V27() real Element of REAL

x * (r . n) is Element of the carrier of X

dist ((x * (r . n)),(x * (X,r))) is ext-real V27() real Element of REAL

(x * (r . n)) - (x * (X,r)) is Element of the carrier of X

||.((x * (r . n)) - (x * (X,r))).|| is ext-real V27() real Element of REAL

(r . n) - (X,r) is Element of the carrier of X

x * ((r . n) - (X,r)) is Element of the carrier of X

||.(x * ((r . n) - (X,r))).|| is ext-real V27() real Element of REAL

||.((r . n) - (X,r)).|| is ext-real V27() real Element of REAL

(abs x) * ||.((r . n) - (X,r)).|| is ext-real V27() real Element of REAL

(abs x) * (dist ((r . n),(X,r))) is ext-real V27() real Element of REAL

(x * r) . n is Element of the carrier of X

dist (((x * r) . n),(x * (X,r))) is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

- x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,(- x)) is Element of the carrier of X

(X,x) is Element of the carrier of X

- (X,x) is Element of the carrier of X

(- 1) * x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,((- 1) * x)) is Element of the carrier of X

(- 1) * (X,x) is Element of the carrier of X

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

r + x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,(r + x)) is Element of the carrier of X

(X,r) is Element of the carrier of X

(X,r) + x is Element of the carrier of X

q is ext-real V27() real Element of REAL

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . n is Element of the carrier of X

dist ((r . n),(X,r)) is ext-real V27() real Element of REAL

- x is Element of the carrier of X

(r . n) - (- x) is Element of the carrier of X

(X,r) - (- x) is Element of the carrier of X

dist (((r . n) - (- x)),((X,r) - (- x))) is ext-real V27() real Element of REAL

- (- x) is Element of the carrier of X

(r . n) + (- (- x)) is Element of the carrier of X

dist (((r . n) + (- (- x))),((X,r) - (- x))) is ext-real V27() real Element of REAL

(r . n) + x is Element of the carrier of X

dist (((r . n) + x),((X,r) - (- x))) is ext-real V27() real Element of REAL

(X,r) + (- (- x)) is Element of the carrier of X

dist (((r . n) + x),((X,r) + (- (- x)))) is ext-real V27() real Element of REAL

dist (((r . n) + x),((X,r) + x)) is ext-real V27() real Element of REAL

(r + x) . n is Element of the carrier of X

dist (((r + x) . n),((X,r) + x)) is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

r - x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,(r - x)) is Element of the carrier of X

(X,r) is Element of the carrier of X

(X,r) - x is Element of the carrier of X

- x is Element of the carrier of X

r + (- x) is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,(r + (- x))) is Element of the carrier of X

(X,r) + (- x) is Element of the carrier of X

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,r) is Element of the carrier of X

y is ext-real V27() real Element of REAL

q is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . n is Element of the carrier of X

(r . n) - x is Element of the carrier of X

||.((r . n) - x).|| is ext-real V27() real Element of REAL

dist ((r . n),x) is ext-real V27() real Element of REAL

y is ext-real V27() real Element of REAL

q is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . n is Element of the carrier of X

(r . n) - x is Element of the carrier of X

||.((r . n) - x).|| is ext-real V27() real Element of REAL

dist ((r . n),x) is ext-real V27() real Element of REAL

y is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

r is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

y is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . y is ext-real V27() real Element of REAL

x . y is Element of the carrier of X

||.(x . y).|| is ext-real V27() real Element of REAL

r is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

y is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

q is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . q is ext-real V27() real Element of REAL

x . q is Element of the carrier of X

||.(x . q).|| is ext-real V27() real Element of REAL

y . q is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,x) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

r is Element of the carrier of X

y is ext-real V27() real set

q is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

x . n is Element of the carrier of X

(x . n) - r is Element of the carrier of X

||.((x . n) - r).|| is ext-real V27() real Element of REAL

||.(x . n).|| is ext-real V27() real Element of REAL

||.r.|| is ext-real V27() real Element of REAL

||.(x . n).|| - ||.r.|| is ext-real V27() real Element of REAL

abs (||.(x . n).|| - ||.r.||) is ext-real V27() real Element of REAL

(X,x) . n is ext-real V27() real Element of REAL

((X,x) . n) - ||.r.|| is ext-real V27() real Element of REAL

abs (((X,x) . n) - ||.r.||) is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(X,x) . n is ext-real V27() real Element of REAL

((X,x) . n) - ||.r.|| is ext-real V27() real Element of REAL

abs (((X,x) . n) - ||.r.||) is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

||.x.|| is ext-real V27() real Element of REAL

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,r) is Element of the carrier of X

(X,r) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,r) is ext-real V27() real Element of REAL

y is ext-real V27() real set

q is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . n is Element of the carrier of X

(r . n) - x is Element of the carrier of X

||.((r . n) - x).|| is ext-real V27() real Element of REAL

||.(r . n).|| is ext-real V27() real Element of REAL

||.(r . n).|| - ||.x.|| is ext-real V27() real Element of REAL

abs (||.(r . n).|| - ||.x.||) is ext-real V27() real Element of REAL

(X,r) . n is ext-real V27() real Element of REAL

((X,r) . n) - ||.x.|| is ext-real V27() real Element of REAL

abs (((X,r) . n) - ||.x.||) is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(X,r) . n is ext-real V27() real Element of REAL

((X,r) . n) - ||.x.|| is ext-real V27() real Element of REAL

abs (((X,r) . n) - ||.x.||) is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,r) is Element of the carrier of X

r - x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,(r - x)) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,(r - x)) is ext-real V27() real Element of REAL

y is ext-real V27() real set

q is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . n is Element of the carrier of X

(r . n) - x is Element of the carrier of X

||.((r . n) - x).|| is ext-real V27() real Element of REAL

0. X is V64(X) Element of the carrier of X

((r . n) - x) - H

||.(((r . n) - x) - H

||.H

||.((r . n) - x).|| - ||.H

abs (||.((r . n) - x).|| - ||.H

||.((r . n) - x).|| - 0 is ext-real V27() real Element of REAL

abs (||.((r . n) - x).|| - 0) is ext-real V27() real Element of REAL

(r - x) . n is Element of the carrier of X

||.((r - x) . n).|| is ext-real V27() real Element of REAL

||.((r - x) . n).|| - 0 is ext-real V27() real Element of REAL

abs (||.((r - x) . n).|| - 0) is ext-real V27() real Element of REAL

(X,(r - x)) . n is ext-real V27() real Element of REAL

((X,(r - x)) . n) - 0 is ext-real V27() real Element of REAL

abs (((X,(r - x)) . n) - 0) is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

r is Element of the carrier of X

y is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

q is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

y . q is ext-real V27() real Element of REAL

x . q is Element of the carrier of X

dist ((x . q),r) is ext-real V27() real Element of REAL

y is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

q is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

y . k is ext-real V27() real Element of REAL

x . k is Element of the carrier of X

dist ((x . k),r) is ext-real V27() real Element of REAL

q . k is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,r) is Element of the carrier of X

(X,r,x) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

y is ext-real V27() real set

q is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . n is Element of the carrier of X

dist ((r . n),x) is ext-real V27() real Element of REAL

(dist ((r . n),x)) - 0 is ext-real V27() real Element of REAL

abs ((dist ((r . n),x)) - 0) is ext-real V27() real Element of REAL

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(X,r,x) . n is ext-real V27() real Element of REAL

((X,r,x) . n) - 0 is ext-real V27() real Element of REAL

abs (((X,r,x) . n) - 0) is ext-real V27() real Element of REAL

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(X,r,x) . n is ext-real V27() real Element of REAL

((X,r,x) . n) - 0 is ext-real V27() real Element of REAL

abs (((X,r,x) . n) - 0) is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,r) is Element of the carrier of X

(X,r,x) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,r,x) is ext-real V27() real Element of REAL

y is ext-real V27() real set

q is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

r . n is Element of the carrier of X

dist ((r . n),x) is ext-real V27() real Element of REAL

(dist ((r . n),x)) - 0 is ext-real V27() real Element of REAL

abs ((dist ((r . n),x)) - 0) is ext-real V27() real Element of REAL

k is ext-real epsilon-transitive epsilon-connected ordinal natural V27() real V125() V126() V127() V128() V129() V130() V131() V132() Element of NAT

(X,r,x) . n is ext-real V27() real Element of REAL

((X,r,x) . n) - 0 is ext-real V27() real Element of REAL

abs (((X,r,x) . n) - 0) is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is Element of the carrier of X

x + r is Element of the carrier of X

||.(x + r).|| is ext-real V27() real Element of REAL

y is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,y) is Element of the carrier of X

q is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,q) is Element of the carrier of X

y + q is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,(y + q)) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,(y + q)) is ext-real V27() real Element of REAL

(X,(y + q)) is Element of the carrier of X

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is Element of the carrier of X

x + r is Element of the carrier of X

y is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,y) is Element of the carrier of X

q is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,q) is Element of the carrier of X

y + q is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(y + q) - (x + r) is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,((y + q) - (x + r))) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,((y + q) - (x + r))) is ext-real V27() real Element of REAL

(X,(y + q)) is Element of the carrier of X

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is Element of the carrier of X

x - r is Element of the carrier of X

||.(x - r).|| is ext-real V27() real Element of REAL

y is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,y) is Element of the carrier of X

q is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,q) is Element of the carrier of X

y - q is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,(y - q)) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,(y - q)) is ext-real V27() real Element of REAL

(X,(y - q)) is Element of the carrier of X

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is Element of the carrier of X

x - r is Element of the carrier of X

y is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,y) is Element of the carrier of X

q is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,q) is Element of the carrier of X

y - q is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(y - q) - (x - r) is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,((y - q) - (x - r))) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,((y - q) - (x - r))) is ext-real V27() real Element of REAL

(X,(y - q)) is Element of the carrier of X

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is ext-real V27() real Element of REAL

r * x is Element of the carrier of X

||.(r * x).|| is ext-real V27() real Element of REAL

y is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,y) is Element of the carrier of X

r * y is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,(r * y)) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,(r * y)) is ext-real V27() real Element of REAL

(X,(r * y)) is Element of the carrier of X

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is ext-real V27() real Element of REAL

r * x is Element of the carrier of X

y is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,y) is Element of the carrier of X

r * y is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(r * y) - (r * x) is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,((r * y) - (r * x))) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,((r * y) - (r * x))) is ext-real V27() real Element of REAL

(X,(r * y)) is Element of the carrier of X

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

- x is Element of the carrier of X

||.(- x).|| is ext-real V27() real Element of REAL

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,r) is Element of the carrier of X

- r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,(- r)) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,(- r)) is ext-real V27() real Element of REAL

(X,(- r)) is Element of the carrier of X

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

- x is Element of the carrier of X

r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,r) is Element of the carrier of X

- r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(- r) - (- x) is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,((- r) - (- x))) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,((- r) - (- x))) is ext-real V27() real Element of REAL

(X,(- r)) is Element of the carrier of X

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is Element of the carrier of X

x + r is Element of the carrier of X

||.(x + r).|| is ext-real V27() real Element of REAL

y is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,y) is Element of the carrier of X

y + r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,(y + r)) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,(y + r)) is ext-real V27() real Element of REAL

(X,(y + r)) is Element of the carrier of X

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is Element of the carrier of X

x + r is Element of the carrier of X

y is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,y) is Element of the carrier of X

y + r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(y + r) - (x + r) is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,((y + r) - (x + r))) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,((y + r) - (x + r))) is ext-real V27() real Element of REAL

(X,(y + r)) is Element of the carrier of X

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is Element of the carrier of X

x - r is Element of the carrier of X

||.(x - r).|| is ext-real V27() real Element of REAL

y is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,y) is Element of the carrier of X

y - r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,(y - r)) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,(y - r)) is ext-real V27() real Element of REAL

- r is Element of the carrier of X

y + (- r) is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,(y + (- r))) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,(y + (- r))) is ext-real V27() real Element of REAL

x + (- r) is Element of the carrier of X

||.(x + (- r)).|| is ext-real V27() real Element of REAL

X is non empty V83() V108() V109() V110() V111() V112() V113() V114() RealUnitarySpace-like UNITSTR

the carrier of X is V4() set

K33(NAT, the carrier of X) is set

K32(K33(NAT, the carrier of X)) is set

x is Element of the carrier of X

r is Element of the carrier of X

x - r is Element of the carrier of X

y is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,y) is Element of the carrier of X

y - r is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(y - r) - (x - r) is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,((y - r) - (x - r))) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,((y - r) - (x - r))) is ext-real V27() real Element of REAL

- r is Element of the carrier of X

y + (- r) is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

x + (- r) is Element of the carrier of X

(y + (- r)) - (x + (- r)) is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,((y + (- r)) - (x + (- r)))) is Relation-like NAT -defined REAL -valued V12() V30( NAT , REAL ) Element of K32(K33(NAT,REAL))

lim (X,((y + (- r)) - (x + (- r)))) is ext-real V27() real Element of REAL

(y - r) - (x + (- r)) is V4() Relation-like NAT -defined the carrier of X -valued V12() V29( NAT ) V30( NAT , the carrier of X) Element of K32(K33(NAT, the carrier of X))

(X,((y - r) - (x + (- r)))) is Relation-like NAT -defined