:: 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₁(X)) is ext-real V27() real Element of REAL
dist (H₁(X),H₁(X)) 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
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₁(X)) is ext-real V27() real Element of REAL
dist (H₁(X),H₁(X)) 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
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₁(X) is Element of the carrier of X
||.(((r . n) - x) - H₁(X)).|| is ext-real V27() real Element of REAL
||.H₁(X).|| is ext-real V27() real Element of REAL
||.((r . n) - x).|| - ||.H₁(X).|| is ext-real V27() real Element of REAL
abs (||.((r . n) - x).|| - ||.H₁(X).||) is ext-real V27() real Element of REAL
||.((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