:: LOPBAN_6 semantic presentation

REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL
bool REAL is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal set
bool omega is non empty set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
[:2,2:] is non empty set
[:[:2,2:],REAL:] is set
bool [:[:2,2:],REAL:] is non empty set
bool NAT is non empty set
[:NAT,REAL:] is set
bool [:NAT,REAL:] is non empty set
COMPLEX is set
RAT is set
INT is set
K483() is non empty set
[:K483(),K483():] is non empty set
[:[:K483(),K483():],K483():] is non empty set
bool [:[:K483(),K483():],K483():] is non empty set
[:REAL,K483():] is set
[:[:REAL,K483():],K483():] is set
bool [:[:REAL,K483():],K483():] is non empty set
K489() is L14()
the carrier of K489() is set
bool the carrier of K489() is non empty set
K493() is Element of bool the carrier of K489()
[:K493(),K493():] is set
[:[:K493(),K493():],REAL:] is set
bool [:[:K493(),K493():],REAL:] is non empty set
the_set_of_l1RealSequences is Element of bool the carrier of K489()
[:the_set_of_l1RealSequences,REAL:] is set
bool [:the_set_of_l1RealSequences,REAL:] is non empty set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative set
0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
- 1 is complex real ext-real non positive Element of REAL
X is complex real ext-real set
Y is complex real ext-real set
T is complex real ext-real set
1 + T is complex real ext-real Element of REAL
Y * (1 + T) is complex real ext-real Element of REAL
Y / (1 + T) is complex real ext-real Element of REAL
T / X is complex real ext-real Element of COMPLEX
(T / X) - 1 is complex real ext-real Element of REAL
1 + ((T / X) - 1) is complex real ext-real Element of REAL
(1 + ((T / X) - 1)) " is complex real ext-real Element of REAL
1 / (1 + ((T / X) - 1)) is complex real ext-real Element of REAL
T * ((1 + ((T / X) - 1)) ") is complex real ext-real Element of REAL
T * 1 is complex real ext-real Element of REAL
(T * 1) / (1 + ((T / X) - 1)) is complex real ext-real Element of REAL
(1 + ((T / X) - 1)) * X is complex real ext-real Element of REAL
X / X is complex real ext-real Element of COMPLEX
(X / X) * T is complex real ext-real set
1 * T is complex real ext-real Element of REAL
((1 + ((T / X) - 1)) ") * (1 + ((T / X) - 1)) is complex real ext-real Element of REAL
(((1 + ((T / X) - 1)) ") * (1 + ((T / X) - 1))) * X is complex real ext-real Element of REAL
Y * (1 + ((T / X) - 1)) is complex real ext-real Element of REAL
Y / (1 + ((T / X) - 1)) is complex real ext-real Element of REAL
1 + T is complex real ext-real Element of REAL
Y / (1 + T) is complex real ext-real Element of REAL
T / X is complex real ext-real Element of COMPLEX
(T / X) - 1 is complex real ext-real Element of REAL
1 + ((T / X) - 1) is complex real ext-real Element of REAL
Y / (1 + ((T / X) - 1)) is complex real ext-real Element of REAL
1 + T is complex real ext-real Element of REAL
Y / (1 + T) is complex real ext-real Element of REAL
T / X is complex real ext-real Element of COMPLEX
(T / X) - 1 is complex real ext-real Element of REAL
1 + ((T / X) - 1) is complex real ext-real Element of REAL
Y / (1 + ((T / X) - 1)) is complex real ext-real Element of REAL
T is complex real ext-real set
1 + T is complex real ext-real Element of REAL
Y / (1 + T) is complex real ext-real Element of REAL
F₁() is non empty set
[:NAT,F₁():] is non empty set
bool [:NAT,F₁():] is non empty set
F₂() is Element of F₁()
F₃() is Element of F₁()
[:F₁(),F₁():] is non empty set
X is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
Y is Element of [:F₁(),F₁():]
Y `1 is set
Y `2 is set
Y `1 is Element of F<sub>1</sub>()
Y `2 is Element of F₁()
TB1 is Element of F₁()
G is Element of F₁()
f is Element of F₁()
[G,f] is V13() Element of [:F₁(),F₁():]
{G,f} is set
{G} is set
{{G,f},{G}} is set
n0 is Element of [:F₁(),F₁():]
n0 `2 is set
n0 `1 is set
[:NAT,[:F₁(),F₁():]:] is non empty set
bool [:NAT,[:F₁(),F₁():]:] is non empty set
[F₂(),F₃()] is V13() Element of [:F₁(),F₁():]
{F₂(),F₃()} is set
{F₂()} is set
{{F₂(),F₃()},{F₂()}} is set
X is non empty V16() V19( NAT ) V20([:F₁(),F₁():]) Function-like V26( NAT ) quasi_total Element of bool [:NAT,[:F₁(),F₁():]:]
X . 0 is Element of [:F₁(),F₁():]
Y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
X . Y is Element of [:F₁(),F₁():]
(X . Y) `1 is Element of F<sub>1</sub>()
Y is non empty V16() V19( NAT ) V20(F<sub>1</sub>()) Function-like V26( NAT ) quasi_total Element of bool [:NAT,F<sub>1</sub>():]
T is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
Y . T is Element of F<sub>1</sub>()
X . T is Element of [:F<sub>1</sub>(),F<sub>1</sub>():]
(X . T) `1 is Element of F₁()
T + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
X . (T + 1) is Element of [:F₁(),F₁():]
(T + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
X . ((T + 1) + 1) is Element of [:F₁(),F₁():]
(X . (T + 1)) `1 is set
(X . (T + 1)) `2 is set
(X . ((T + 1) + 1)) `2 is set
(X . ((T + 1) + 1)) `1 is set
T + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
Y . (T + 2) is Element of F₁()
(X . (T + 1)) `2 is Element of F<sub>1</sub>()
Y . (T + 1) is Element of F<sub>1</sub>()
(X . (T + 1)) `1 is Element of F₁()
(X . T) `2 is Element of F<sub>1</sub>()
Y . 0 is Element of F<sub>1</sub>()
Y . 1 is Element of F<sub>1</sub>()
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
X . (0 + 1) is Element of [:F<sub>1</sub>(),F<sub>1</sub>():]
(X . 0) `1 is set
(X . 0) `2 is set
(X . (0 + 1)) `2 is set
(X . (0 + 1)) `1 is set
(X . 0) `1 is Element of F₁()
X . 1 is Element of [:F₁(),F₁():]
(X . 1) `1 is Element of F₁()
T is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
Y . T is Element of F₁()
T + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
Y . (T + 1) is Element of F₁()
T + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
Y . (T + 2) is Element of F₁()
X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of X is non empty set
0. X is zero Element of the carrier of X
Y is Element of the carrier of X
T is complex real ext-real set
Ball (Y,T) is Element of bool the carrier of X
bool the carrier of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : not T <= ||.(Y - b₁).|| } is set
Ball ((0. X),T) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not T <= ||.((0. X) - b₁).|| } is set
Y + (Ball ((0. X),T)) is Element of bool the carrier of X
{ K230(X,Y,b₁) where b₁ is Element of the carrier of X : b₁ in Ball ((0. X),T) } is set
T1 is set
TB1 is Element of the carrier of X
TB1 - Y is Element of the carrier of X
- Y is Element of the carrier of X
K230(X,TB1,(- Y)) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,TB1,(- Y)) is Element of the carrier of X
- (TB1 - Y) is Element of the carrier of X
||.(- (TB1 - Y)).|| is complex real ext-real non negative Element of REAL
f is Element of the carrier of X
Y - f is Element of the carrier of X
- f is Element of the carrier of X
K230(X,Y,(- f)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,Y,(- f)) is Element of the carrier of X
||.(Y - f).|| is complex real ext-real non negative Element of REAL
(0. X) - (TB1 - Y) is Element of the carrier of X
K230(X,(0. X),(- (TB1 - Y))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(0. X),(- (TB1 - Y))) is Element of the carrier of X
||.((0. X) - (TB1 - Y)).|| is complex real ext-real non negative Element of REAL
(TB1 - Y) + Y is Element of the carrier of X
K179( the carrier of X, the U7 of X,(TB1 - Y),Y) is Element of the carrier of X
(- Y) + Y is Element of the carrier of X
K179( the carrier of X, the U7 of X,(- Y),Y) is Element of the carrier of X
TB1 + ((- Y) + Y) is Element of the carrier of X
K179( the carrier of X, the U7 of X,TB1,((- Y) + Y)) is Element of the carrier of X
TB1 + (0. X) is Element of the carrier of X
K179( the carrier of X, the U7 of X,TB1,(0. X)) is Element of the carrier of X
T1 is set
TB1 is Element of the carrier of X
Y + TB1 is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,Y,TB1) is Element of the carrier of X
TB1 + Y is Element of the carrier of X
K179( the carrier of X, the U7 of X,TB1,Y) is Element of the carrier of X
- TB1 is Element of the carrier of X
||.(- TB1).|| is complex real ext-real non negative Element of REAL
f is Element of the carrier of X
(0. X) - f is Element of the carrier of X
- f is Element of the carrier of X
K230(X,(0. X),(- f)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(0. X),(- f)) is Element of the carrier of X
||.((0. X) - f).|| is complex real ext-real non negative Element of REAL
||.TB1.|| is complex real ext-real non negative Element of REAL
TB1 + (0. X) is Element of the carrier of X
K179( the carrier of X, the U7 of X,TB1,(0. X)) is Element of the carrier of X
||.(TB1 + (0. X)).|| is complex real ext-real non negative Element of REAL
- Y is Element of the carrier of X
Y + (- Y) is Element of the carrier of X
K179( the carrier of X, the U7 of X,Y,(- Y)) is Element of the carrier of X
TB1 + (Y + (- Y)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,TB1,(Y + (- Y))) is Element of the carrier of X
||.(TB1 + (Y + (- Y))).|| is complex real ext-real non negative Element of REAL
(TB1 + Y) - Y is Element of the carrier of X
K230(X,(TB1 + Y),(- Y)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(TB1 + Y),(- Y)) is Element of the carrier of X
||.((TB1 + Y) - Y).|| is complex real ext-real non negative Element of REAL
Y - (TB1 + Y) is Element of the carrier of X
- (TB1 + Y) is Element of the carrier of X
K230(X,Y,(- (TB1 + Y))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,Y,(- (TB1 + Y))) is Element of the carrier of X
||.(Y - (TB1 + Y)).|| is complex real ext-real non negative Element of REAL
X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
0. X is zero Element of the carrier of X
the carrier of X is non empty set
Y is complex real ext-real set
Ball ((0. X),Y) is Element of bool the carrier of X
bool the carrier of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : not Y <= ||.((0. X) - b₁).|| } is set
T is complex real ext-real Element of REAL
T * Y is complex real ext-real Element of REAL
Ball ((0. X),(T * Y)) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not T * Y <= ||.((0. X) - b₁).|| } is set
T * (Ball ((0. X),Y)) is Element of bool the carrier of X
{ (T * b₁) where b₁ is Element of the carrier of X : b₁ in Ball ((0. X),Y) } is set
T1 is set
TB1 is Element of the carrier of X
- TB1 is Element of the carrier of X
||.(- TB1).|| is complex real ext-real non negative Element of REAL
G is Element of the carrier of X
(0. X) - G is Element of the carrier of X
- G is Element of the carrier of X
K230(X,(0. X),(- G)) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,(0. X),(- G)) is Element of the carrier of X
||.((0. X) - G).|| is complex real ext-real non negative Element of REAL
||.TB1.|| is complex real ext-real non negative Element of REAL
T " is complex real ext-real Element of REAL
(T ") * (T * Y) is complex real ext-real Element of REAL
(T ") * ||.TB1.|| is complex real ext-real Element of REAL
T * (T ") is complex real ext-real Element of REAL
(T * (T ")) * Y is complex real ext-real Element of REAL
1 * Y is complex real ext-real Element of REAL
(T ") * TB1 is Element of the carrier of X
the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is set
[:[:REAL, the carrier of X:], the carrier of X:] is set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K175( the U9 of X,(T "),TB1) is set
||.((T ") * TB1).|| is complex real ext-real non negative Element of REAL
abs (T ") is complex real ext-real Element of REAL
(abs (T ")) * ||.TB1.|| is complex real ext-real Element of REAL
- ((T ") * TB1) is Element of the carrier of X
||.(- ((T ") * TB1)).|| is complex real ext-real non negative Element of REAL
(0. X) - ((T ") * TB1) is Element of the carrier of X
K230(X,(0. X),(- ((T ") * TB1))) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,(0. X),(- ((T ") * TB1))) is Element of the carrier of X
||.((0. X) - ((T ") * TB1)).|| is complex real ext-real non negative Element of REAL
T * ((T ") * TB1) is Element of the carrier of X
K175( the U9 of X,T,((T ") * TB1)) is set
(T * (T ")) * TB1 is Element of the carrier of X
K175( the U9 of X,(T * (T ")),TB1) is set
1 * TB1 is Element of the carrier of X
K175( the U9 of X,1,TB1) is set
T1 is set
TB1 is Element of the carrier of X
G is Element of the carrier of X
T * G is Element of the carrier of X
the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is set
[:[:REAL, the carrier of X:], the carrier of X:] is set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K175( the U9 of X,T,G) is set
- G is Element of the carrier of X
||.(- G).|| is complex real ext-real non negative Element of REAL
f is Element of the carrier of X
(0. X) - f is Element of the carrier of X
- f is Element of the carrier of X
K230(X,(0. X),(- f)) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,(0. X),(- f)) is Element of the carrier of X
||.((0. X) - f).|| is complex real ext-real non negative Element of REAL
||.G.|| is complex real ext-real non negative Element of REAL
||.TB1.|| is complex real ext-real non negative Element of REAL
abs T is complex real ext-real Element of REAL
(abs T) * ||.G.|| is complex real ext-real Element of REAL
T * ||.G.|| is complex real ext-real Element of REAL
- TB1 is Element of the carrier of X
||.(- TB1).|| is complex real ext-real non negative Element of REAL
(0. X) - TB1 is Element of the carrier of X
K230(X,(0. X),(- TB1)) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,(0. X),(- TB1)) is Element of the carrier of X
||.((0. X) - TB1).|| is complex real ext-real non negative Element of REAL
X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
Y is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
T is non empty V16() V19( the carrier of X) V20( the carrier of Y) Function-like V26( the carrier of X) quasi_total V231(X,Y) V232(X,Y) Element of bool [: the carrier of X, the carrier of Y:]
T1 is Element of bool the carrier of X
TB1 is Element of bool the carrier of X
T1 + TB1 is Element of bool the carrier of X
{ K230(X,b₁,b₂) where b₁, b₂ is Element of the carrier of X : ( b₁ in T1 & b₂ in TB1 ) } is set
T .: (T1 + TB1) is Element of bool the carrier of Y
bool the carrier of Y is non empty set
T .: T1 is Element of bool the carrier of Y
T .: TB1 is Element of bool the carrier of Y
(T .: T1) + (T .: TB1) is Element of bool the carrier of Y
{ K230(Y,b₁,b₂) where b₁, b₂ is Element of the carrier of Y : ( b₁ in T .: T1 & b₂ in T .: TB1 ) } is set
G is set
f is set
T . f is set
f is Element of the carrier of X
n0 is Element of the carrier of X
f + n0 is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,f,n0) is Element of the carrier of X
T . f is Element of the carrier of Y
T . n0 is Element of the carrier of Y
(T . f) + (T . n0) is Element of the carrier of Y
the U7 of Y is non empty V16() V19([: the carrier of Y, the carrier of Y:]) V20( the carrier of Y) Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K179( the carrier of Y, the U7 of Y,(T . f),(T . n0)) is Element of the carrier of Y
G is set
f is Element of the carrier of Y
f is Element of the carrier of Y
f + f is Element of the carrier of Y
the U7 of Y is non empty V16() V19([: the carrier of Y, the carrier of Y:]) V20( the carrier of Y) Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K179( the carrier of Y, the U7 of Y,f,f) is Element of the carrier of Y
n0 is Element of the carrier of X
T . n0 is Element of the carrier of Y
r is Element of the carrier of X
T . r is Element of the carrier of Y
TBn0 is Element of the carrier of X
y0 is Element of the carrier of X
TBn0 + y0 is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,TBn0,y0) is Element of the carrier of X
T . (TBn0 + y0) is Element of the carrier of Y
X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
Y is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
T is non empty V16() V19( the carrier of X) V20( the carrier of Y) Function-like V26( the carrier of X) quasi_total V231(X,Y) V232(X,Y) Element of bool [: the carrier of X, the carrier of Y:]
T1 is Element of bool the carrier of X
T .: T1 is Element of bool the carrier of Y
bool the carrier of Y is non empty set
TB1 is complex real ext-real Element of REAL
TB1 * T1 is Element of bool the carrier of X
{ (TB1 * b₁) where b₁ is Element of the carrier of X : b₁ in T1 } is set
T .: (TB1 * T1) is Element of bool the carrier of Y
TB1 * (T .: T1) is Element of bool the carrier of Y
{ (TB1 * b₁) where b₁ is Element of the carrier of Y : b₁ in T .: T1 } is set
G is set
f is set
T . f is set
f is Element of the carrier of X
TB1 * f is Element of the carrier of X
the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is set
[:[:REAL, the carrier of X:], the carrier of X:] is set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K175( the U9 of X,TB1,f) is set
T . f is Element of the carrier of Y
TB1 * (T . f) is Element of the carrier of Y
the U9 of Y is V16() V19([:REAL, the carrier of Y:]) V20( the carrier of Y) Function-like V26([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is set
[:[:REAL, the carrier of Y:], the carrier of Y:] is set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
K175( the U9 of Y,TB1,(T . f)) is set
G is set
f is Element of the carrier of Y
TB1 * f is Element of the carrier of Y
the U9 of Y is V16() V19([:REAL, the carrier of Y:]) V20( the carrier of Y) Function-like V26([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is set
[:[:REAL, the carrier of Y:], the carrier of Y:] is set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
K175( the U9 of Y,TB1,f) is set
f is Element of the carrier of X
T . f is Element of the carrier of Y
n0 is Element of the carrier of X
TB1 * n0 is Element of the carrier of X
the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is set
[:[:REAL, the carrier of X:], the carrier of X:] is set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K175( the U9 of X,TB1,n0) is set
T . (TB1 * n0) is Element of the carrier of Y
X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
Y is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
T is non empty V16() V19( the carrier of X) V20( the carrier of Y) Function-like V26( the carrier of X) quasi_total V231(X,Y) V232(X,Y) Element of bool [: the carrier of X, the carrier of Y:]
T1 is Element of bool the carrier of X
T .: T1 is Element of bool the carrier of Y
bool the carrier of Y is non empty set
TB1 is Element of the carrier of X
TB1 + T1 is Element of bool the carrier of X
{ K230(X,TB1,b₁) where b₁ is Element of the carrier of X : b₁ in T1 } is set
T .: (TB1 + T1) is Element of bool the carrier of Y
T . TB1 is Element of the carrier of Y
(T . TB1) + (T .: T1) is Element of bool the carrier of Y
{ K230(Y,(T . TB1),b₁) where b₁ is Element of the carrier of Y : b₁ in T .: T1 } is set
G is set
f is set
T . f is set
f is Element of the carrier of X
n0 is Element of the carrier of X
TB1 + n0 is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,TB1,n0) is Element of the carrier of X
T . n0 is Element of the carrier of Y
(T . TB1) + (T . n0) is Element of the carrier of Y
the U7 of Y is non empty V16() V19([: the carrier of Y, the carrier of Y:]) V20( the carrier of Y) Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K179( the carrier of Y, the U7 of Y,(T . TB1),(T . n0)) is Element of the carrier of Y
G is set
f is Element of the carrier of Y
(T . TB1) + f is Element of the carrier of Y
the U7 of Y is non empty V16() V19([: the carrier of Y, the carrier of Y:]) V20( the carrier of Y) Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K179( the carrier of Y, the U7 of Y,(T . TB1),f) is Element of the carrier of Y
f is Element of the carrier of X
T . f is Element of the carrier of Y
TB1 + f is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,TB1,f) is Element of the carrier of X
T . (TB1 + f) is Element of the carrier of Y
X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
LinearTopSpaceNorm X is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()
the carrier of (LinearTopSpaceNorm X) is non empty set
bool the carrier of (LinearTopSpaceNorm X) is non empty set
Y is Element of bool the carrier of X
T is Element of bool the carrier of X
Y + T is Element of bool the carrier of X
{ K230(X,b₁,b₂) where b₁, b₂ is Element of the carrier of X : ( b₁ in Y & b₂ in T ) } is set
T1 is Element of bool the carrier of (LinearTopSpaceNorm X)
TB1 is Element of bool the carrier of (LinearTopSpaceNorm X)
T1 + TB1 is Element of bool the carrier of (LinearTopSpaceNorm X)
{ K230((LinearTopSpaceNorm X),b₁,b₂) where b₁, b₂ is Element of the carrier of (LinearTopSpaceNorm X) : ( b₁ in T1 & b₂ in TB1 ) } is set
G is set
f is Element of the carrier of X
f is Element of the carrier of X
f + f is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,f,f) is Element of the carrier of X
r is Element of the carrier of (LinearTopSpaceNorm X)
n0 is Element of the carrier of (LinearTopSpaceNorm X)
r + n0 is Element of the carrier of (LinearTopSpaceNorm X)
the U7 of (LinearTopSpaceNorm X) is non empty V16() V19([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]
[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):] is non empty set
[:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
K179( the carrier of (LinearTopSpaceNorm X), the U7 of (LinearTopSpaceNorm X),r,n0) is Element of the carrier of (LinearTopSpaceNorm X)
G is set
f is Element of the carrier of (LinearTopSpaceNorm X)
f is Element of the carrier of (LinearTopSpaceNorm X)
f + f is Element of the carrier of (LinearTopSpaceNorm X)
the U7 of (LinearTopSpaceNorm X) is non empty V16() V19([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]
[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):] is non empty set
[:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
K179( the carrier of (LinearTopSpaceNorm X), the U7 of (LinearTopSpaceNorm X),f,f) is Element of the carrier of (LinearTopSpaceNorm X)
r is Element of the carrier of X
n0 is Element of the carrier of X
r + n0 is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,r,n0) is Element of the carrier of X
X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
LinearTopSpaceNorm X is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()
the carrier of (LinearTopSpaceNorm X) is non empty set
bool the carrier of (LinearTopSpaceNorm X) is non empty set
Y is Element of bool the carrier of X
T is Element of the carrier of X
T + Y is Element of bool the carrier of X
{ K230(X,T,b₁) where b₁ is Element of the carrier of X : b₁ in Y } is set
T1 is Element of bool the carrier of (LinearTopSpaceNorm X)
TB1 is Element of the carrier of (LinearTopSpaceNorm X)
TB1 + T1 is Element of bool the carrier of (LinearTopSpaceNorm X)
{ K230((LinearTopSpaceNorm X),TB1,b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm X) : b₁ in T1 } is set
G is set
f is Element of the carrier of X
T + f is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,T,f) is Element of the carrier of X
f is Element of the carrier of (LinearTopSpaceNorm X)
TB1 + f is Element of the carrier of (LinearTopSpaceNorm X)
the U7 of (LinearTopSpaceNorm X) is non empty V16() V19([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]
[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):] is non empty set
[:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
K179( the carrier of (LinearTopSpaceNorm X), the U7 of (LinearTopSpaceNorm X),TB1,f) is Element of the carrier of (LinearTopSpaceNorm X)
G is set
f is Element of the carrier of (LinearTopSpaceNorm X)
TB1 + f is Element of the carrier of (LinearTopSpaceNorm X)
the U7 of (LinearTopSpaceNorm X) is non empty V16() V19([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]
[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):] is non empty set
[:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
K179( the carrier of (LinearTopSpaceNorm X), the U7 of (LinearTopSpaceNorm X),TB1,f) is Element of the carrier of (LinearTopSpaceNorm X)
f is Element of the carrier of X
T + f is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,T,f) is Element of the carrier of X
X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of X is non empty set
bool the carrier of X is non empty set
LinearTopSpaceNorm X is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()
the carrier of (LinearTopSpaceNorm X) is non empty set
bool the carrier of (LinearTopSpaceNorm X) is non empty set
Y is Element of bool the carrier of X
T is complex real ext-real Element of REAL
T * Y is Element of bool the carrier of X
{ (T * b₁) where b₁ is Element of the carrier of X : b₁ in Y } is set
T1 is Element of bool the carrier of (LinearTopSpaceNorm X)
T * T1 is Element of bool the carrier of (LinearTopSpaceNorm X)
{ (T * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm X) : b₁ in T1 } is set
TB1 is set
G is Element of the carrier of X
T * G is Element of the carrier of X
the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is set
[:[:REAL, the carrier of X:], the carrier of X:] is set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K175( the U9 of X,T,G) is set
f is Element of the carrier of (LinearTopSpaceNorm X)
T * f is Element of the carrier of (LinearTopSpaceNorm X)
the U9 of (LinearTopSpaceNorm X) is V16() V19([:REAL, the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([:REAL, the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]
[:REAL, the carrier of (LinearTopSpaceNorm X):] is set
[:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is set
bool [:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
K175( the U9 of (LinearTopSpaceNorm X),T,f) is set
TB1 is set
G is Element of the carrier of (LinearTopSpaceNorm X)
T * G is Element of the carrier of (LinearTopSpaceNorm X)
the U9 of (LinearTopSpaceNorm X) is V16() V19([:REAL, the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([:REAL, the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]
[:REAL, the carrier of (LinearTopSpaceNorm X):] is set
[:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is set
bool [:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
K175( the U9 of (LinearTopSpaceNorm X),T,G) is set
f is Element of the carrier of X
T * f is Element of the carrier of X
the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is set
[:[:REAL, the carrier of X:], the carrier of X:] is set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K175( the U9 of X,T,f) is set
X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
TopSpaceNorm X is non empty TopSpace-like TopStruct
MetricSpaceNorm X is non empty V88() V89() V90() V91() L7()
the carrier of X is non empty set
distance_by_norm_of X is V16() V19([: the carrier of X, the carrier of X:]) V20( REAL ) Function-like quasi_total Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:],REAL:] is set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
G7( the carrier of X,(distance_by_norm_of X)) is V83() L7()
K210((MetricSpaceNorm X)) is TopStruct
the carrier of (MetricSpaceNorm X) is non empty set
K209((MetricSpaceNorm X)) is Element of bool (bool the carrier of (MetricSpaceNorm X))
bool the carrier of (MetricSpaceNorm X) is non empty set
bool (bool the carrier of (MetricSpaceNorm X)) is non empty set
TopStruct(# the carrier of (MetricSpaceNorm X),K209((MetricSpaceNorm X)) #) is strict TopStruct
the carrier of (TopSpaceNorm X) is non empty set
bool the carrier of (TopSpaceNorm X) is non empty set
LinearTopSpaceNorm X is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()
the carrier of (LinearTopSpaceNorm X) is non empty set
bool the carrier of (LinearTopSpaceNorm X) is non empty set
Y is Element of bool the carrier of (TopSpaceNorm X)
Cl Y is closed Element of bool the carrier of (TopSpaceNorm X)
T is Element of bool the carrier of (LinearTopSpaceNorm X)
Cl T is closed Element of bool the carrier of (LinearTopSpaceNorm X)
T1 is set
TB1 is Element of bool the carrier of (LinearTopSpaceNorm X)
bool the carrier of X is non empty set
G is Element of bool the carrier of X
f is Element of bool the carrier of (TopSpaceNorm X)
T1 is set
TB1 is Element of bool the carrier of (TopSpaceNorm X)
bool the carrier of X is non empty set
G is Element of bool the carrier of X
f is Element of bool the carrier of (LinearTopSpaceNorm X)
X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of X is non empty set
0. X is zero Element of the carrier of X
T is complex real ext-real set
Ball ((0. X),T) is Element of bool the carrier of X
bool the carrier of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : not T <= ||.((0. X) - b₁).|| } is set
(- 1) * (Ball ((0. X),T)) is Element of bool the carrier of X
{ ((- 1) * b₁) where b₁ is Element of the carrier of X : b₁ in Ball ((0. X),T) } is set
T1 is set
TB1 is Element of the carrier of X
- TB1 is Element of the carrier of X
||.(- TB1).|| is complex real ext-real non negative Element of REAL
G is Element of the carrier of X
(0. X) - G is Element of the carrier of X
- G is Element of the carrier of X
K230(X,(0. X),(- G)) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,(0. X),(- G)) is Element of the carrier of X
||.((0. X) - G).|| is complex real ext-real non negative Element of REAL
- (- TB1) is Element of the carrier of X
||.(- (- TB1)).|| is complex real ext-real non negative Element of REAL
(0. X) - (- TB1) is Element of the carrier of X
K230(X,(0. X),(- (- TB1))) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,(0. X),(- (- TB1))) is Element of the carrier of X
||.((0. X) - (- TB1)).|| is complex real ext-real non negative Element of REAL
(- 1) * (- TB1) is Element of the carrier of X
the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is set
[:[:REAL, the carrier of X:], the carrier of X:] is set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K175( the U9 of X,(- 1),(- TB1)) is set
1 * TB1 is Element of the carrier of X
K175( the U9 of X,1,TB1) is set
T1 is set
TB1 is Element of the carrier of X
G is Element of the carrier of X
(- 1) * G is Element of the carrier of X
the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is set
[:[:REAL, the carrier of X:], the carrier of X:] is set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K175( the U9 of X,(- 1),G) is set
- G is Element of the carrier of X
||.(- G).|| is complex real ext-real non negative Element of REAL
f is Element of the carrier of X
(0. X) - f is Element of the carrier of X
- f is Element of the carrier of X
K230(X,(0. X),(- f)) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,(0. X),(- f)) is Element of the carrier of X
||.((0. X) - f).|| is complex real ext-real non negative Element of REAL
- (- G) is Element of the carrier of X
||.(- (- G)).|| is complex real ext-real non negative Element of REAL
(0. X) - (- G) is Element of the carrier of X
K230(X,(0. X),(- (- G))) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,(0. X),(- (- G))) is Element of the carrier of X
||.((0. X) - (- G)).|| is complex real ext-real non negative Element of REAL
X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of X is non empty set
LinearTopSpaceNorm X is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()
the carrier of (LinearTopSpaceNorm X) is non empty set
bool the carrier of (LinearTopSpaceNorm X) is non empty set
Y is Element of the carrier of X
T is complex real ext-real set
Ball (Y,T) is Element of bool the carrier of X
bool the carrier of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : not T <= ||.(Y - b₁).|| } is set
T1 is Element of bool the carrier of (LinearTopSpaceNorm X)
TB1 is Element of bool the carrier of X
G is Element of the carrier of X
f is Element of the carrier of X
f is complex real ext-real Element of REAL
f * G is Element of the carrier of X
the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is set
[:[:REAL, the carrier of X:], the carrier of X:] is set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K175( the U9 of X,f,G) is set
1 - f is complex real ext-real Element of REAL
(1 - f) * f is Element of the carrier of X
K175( the U9 of X,(1 - f),f) is set
(f * G) + ((1 - f) * f) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,(f * G),((1 - f) * f)) is Element of the carrier of X
abs f is complex real ext-real Element of REAL
(abs f) * T is complex real ext-real Element of REAL
Y - G is Element of the carrier of X
- G is Element of the carrier of X
K230(X,Y,(- G)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,Y,(- G)) is Element of the carrier of X
||.(Y - G).|| is complex real ext-real non negative Element of REAL
(abs f) * ||.(Y - G).|| is complex real ext-real Element of REAL
n0 is Element of the carrier of X
Y - n0 is Element of the carrier of X
- n0 is Element of the carrier of X
K230(X,Y,(- n0)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,Y,(- n0)) is Element of the carrier of X
||.(Y - n0).|| is complex real ext-real non negative Element of REAL
f + 0 is complex real ext-real Element of REAL
abs (1 - f) is complex real ext-real Element of REAL
(abs (1 - f)) * T is complex real ext-real Element of REAL
Y - f is Element of the carrier of X
- f is Element of the carrier of X
K230(X,Y,(- f)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,Y,(- f)) is Element of the carrier of X
||.(Y - f).|| is complex real ext-real non negative Element of REAL
(abs (1 - f)) * ||.(Y - f).|| is complex real ext-real Element of REAL
n0 is Element of the carrier of X
Y - n0 is Element of the carrier of X
- n0 is Element of the carrier of X
K230(X,Y,(- n0)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,Y,(- n0)) is Element of the carrier of X
||.(Y - n0).|| is complex real ext-real non negative Element of REAL
((abs f) * T) + ((abs (1 - f)) * T) is complex real ext-real Element of REAL
((abs f) * ||.(Y - G).||) + ((abs (1 - f)) * ||.(Y - f).||) is complex real ext-real Element of REAL
f * T is complex real ext-real Element of REAL
(f * T) + ((abs (1 - f)) * T) is complex real ext-real Element of REAL
(1 - f) * T is complex real ext-real Element of REAL
(f * T) + ((1 - f) * T) is complex real ext-real Element of REAL
1 * T is complex real ext-real Element of REAL
f * (Y - G) is Element of the carrier of X
K175( the U9 of X,f,(Y - G)) is set
||.(f * (Y - G)).|| is complex real ext-real non negative Element of REAL
||.(f * (Y - G)).|| + ((abs (1 - f)) * ||.(Y - f).||) is complex real ext-real Element of REAL
(1 - f) * (Y - f) is Element of the carrier of X
K175( the U9 of X,(1 - f),(Y - f)) is set
||.((1 - f) * (Y - f)).|| is complex real ext-real non negative Element of REAL
||.(f * (Y - G)).|| + ||.((1 - f) * (Y - f)).|| is complex real ext-real non negative Element of REAL
f * Y is Element of the carrier of X
K175( the U9 of X,f,Y) is set
(1 - f) * Y is Element of the carrier of X
K175( the U9 of X,(1 - f),Y) is set
(f * Y) + ((1 - f) * Y) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(f * Y),((1 - f) * Y)) is Element of the carrier of X
((f * Y) + ((1 - f) * Y)) - ((f * G) + ((1 - f) * f)) is Element of the carrier of X
- ((f * G) + ((1 - f) * f)) is Element of the carrier of X
K230(X,((f * Y) + ((1 - f) * Y)),(- ((f * G) + ((1 - f) * f)))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,((f * Y) + ((1 - f) * Y)),(- ((f * G) + ((1 - f) * f)))) is Element of the carrier of X
||.(((f * Y) + ((1 - f) * Y)) - ((f * G) + ((1 - f) * f))).|| is complex real ext-real non negative Element of REAL
(f * Y) + (- ((f * G) + ((1 - f) * f))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(f * Y),(- ((f * G) + ((1 - f) * f)))) is Element of the carrier of X
((f * Y) + (- ((f * G) + ((1 - f) * f)))) + ((1 - f) * Y) is Element of the carrier of X
K179( the carrier of X, the U7 of X,((f * Y) + (- ((f * G) + ((1 - f) * f)))),((1 - f) * Y)) is Element of the carrier of X
||.(((f * Y) + (- ((f * G) + ((1 - f) * f)))) + ((1 - f) * Y)).|| is complex real ext-real non negative Element of REAL
(- 1) * ((f * G) + ((1 - f) * f)) is Element of the carrier of X
K175( the U9 of X,(- 1),((f * G) + ((1 - f) * f))) is set
(f * Y) + ((- 1) * ((f * G) + ((1 - f) * f))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(f * Y),((- 1) * ((f * G) + ((1 - f) * f)))) is Element of the carrier of X
((f * Y) + ((- 1) * ((f * G) + ((1 - f) * f)))) + ((1 - f) * Y) is Element of the carrier of X
K179( the carrier of X, the U7 of X,((f * Y) + ((- 1) * ((f * G) + ((1 - f) * f)))),((1 - f) * Y)) is Element of the carrier of X
||.(((f * Y) + ((- 1) * ((f * G) + ((1 - f) * f)))) + ((1 - f) * Y)).|| is complex real ext-real non negative Element of REAL
(- 1) * (f * G) is Element of the carrier of X
K175( the U9 of X,(- 1),(f * G)) is set
(- 1) * ((1 - f) * f) is Element of the carrier of X
K175( the U9 of X,(- 1),((1 - f) * f)) is set
((- 1) * (f * G)) + ((- 1) * ((1 - f) * f)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,((- 1) * (f * G)),((- 1) * ((1 - f) * f))) is Element of the carrier of X
(f * Y) + (((- 1) * (f * G)) + ((- 1) * ((1 - f) * f))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(f * Y),(((- 1) * (f * G)) + ((- 1) * ((1 - f) * f)))) is Element of the carrier of X
((f * Y) + (((- 1) * (f * G)) + ((- 1) * ((1 - f) * f)))) + ((1 - f) * Y) is Element of the carrier of X
K179( the carrier of X, the U7 of X,((f * Y) + (((- 1) * (f * G)) + ((- 1) * ((1 - f) * f)))),((1 - f) * Y)) is Element of the carrier of X
||.(((f * Y) + (((- 1) * (f * G)) + ((- 1) * ((1 - f) * f)))) + ((1 - f) * Y)).|| is complex real ext-real non negative Element of REAL
- (f * G) is Element of the carrier of X
(- (f * G)) + ((- 1) * ((1 - f) * f)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(- (f * G)),((- 1) * ((1 - f) * f))) is Element of the carrier of X
(f * Y) + ((- (f * G)) + ((- 1) * ((1 - f) * f))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(f * Y),((- (f * G)) + ((- 1) * ((1 - f) * f)))) is Element of the carrier of X
((f * Y) + ((- (f * G)) + ((- 1) * ((1 - f) * f)))) + ((1 - f) * Y) is Element of the carrier of X
K179( the carrier of X, the U7 of X,((f * Y) + ((- (f * G)) + ((- 1) * ((1 - f) * f)))),((1 - f) * Y)) is Element of the carrier of X
||.(((f * Y) + ((- (f * G)) + ((- 1) * ((1 - f) * f)))) + ((1 - f) * Y)).|| is complex real ext-real non negative Element of REAL
- ((1 - f) * f) is Element of the carrier of X
(- (f * G)) + (- ((1 - f) * f)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(- (f * G)),(- ((1 - f) * f))) is Element of the carrier of X
(f * Y) + ((- (f * G)) + (- ((1 - f) * f))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(f * Y),((- (f * G)) + (- ((1 - f) * f)))) is Element of the carrier of X
((f * Y) + ((- (f * G)) + (- ((1 - f) * f)))) + ((1 - f) * Y) is Element of the carrier of X
K179( the carrier of X, the U7 of X,((f * Y) + ((- (f * G)) + (- ((1 - f) * f)))),((1 - f) * Y)) is Element of the carrier of X
||.(((f * Y) + ((- (f * G)) + (- ((1 - f) * f)))) + ((1 - f) * Y)).|| is complex real ext-real non negative Element of REAL
(f * Y) + (- (f * G)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(f * Y),(- (f * G))) is Element of the carrier of X
((f * Y) + (- (f * G))) + (- ((1 - f) * f)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,((f * Y) + (- (f * G))),(- ((1 - f) * f))) is Element of the carrier of X
(((f * Y) + (- (f * G))) + (- ((1 - f) * f))) + ((1 - f) * Y) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(((f * Y) + (- (f * G))) + (- ((1 - f) * f))),((1 - f) * Y)) is Element of the carrier of X
||.((((f * Y) + (- (f * G))) + (- ((1 - f) * f))) + ((1 - f) * Y)).|| is complex real ext-real non negative Element of REAL
(f * Y) - (f * G) is Element of the carrier of X
K230(X,(f * Y),(- (f * G))) is Element of the carrier of X
((1 - f) * Y) - ((1 - f) * f) is Element of the carrier of X
K230(X,((1 - f) * Y),(- ((1 - f) * f))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,((1 - f) * Y),(- ((1 - f) * f))) is Element of the carrier of X
((f * Y) - (f * G)) + (((1 - f) * Y) - ((1 - f) * f)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,((f * Y) - (f * G)),(((1 - f) * Y) - ((1 - f) * f))) is Element of the carrier of X
||.(((f * Y) - (f * G)) + (((1 - f) * Y) - ((1 - f) * f))).|| is complex real ext-real non negative Element of REAL
(f * (Y - G)) + (((1 - f) * Y) - ((1 - f) * f)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(f * (Y - G)),(((1 - f) * Y) - ((1 - f) * f))) is Element of the carrier of X
||.((f * (Y - G)) + (((1 - f) * Y) - ((1 - f) * f))).|| is complex real ext-real non negative Element of REAL
(f * (Y - G)) + ((1 - f) * (Y - f)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(f * (Y - G)),((1 - f) * (Y - f))) is Element of the carrier of X
||.((f * (Y - G)) + ((1 - f) * (Y - f))).|| is complex real ext-real non negative Element of REAL
f + (1 - f) is complex real ext-real Element of REAL
(f + (1 - f)) * Y is Element of the carrier of X
K175( the U9 of X,(f + (1 - f)),Y) is set
((f + (1 - f)) * Y) - ((f * G) + ((1 - f) * f)) is Element of the carrier of X
K230(X,((f + (1 - f)) * Y),(- ((f * G) + ((1 - f) * f)))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,((f + (1 - f)) * Y),(- ((f * G) + ((1 - f) * f)))) is Element of the carrier of X
||.(((f + (1 - f)) * Y) - ((f * G) + ((1 - f) * f))).|| is complex real ext-real non negative Element of REAL
Y - ((f * G) + ((1 - f) * f)) is Element of the carrier of X
K230(X,Y,(- ((f * G) + ((1 - f) * f)))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,Y,(- ((f * G) + ((1 - f) * f)))) is Element of the carrier of X
||.(Y - ((f * G) + ((1 - f) * f))).|| is complex real ext-real non negative Element of REAL
G is Element of the carrier of (LinearTopSpaceNorm X)
f is Element of the carrier of (LinearTopSpaceNorm X)
f is complex real ext-real Element of REAL
f * G is Element of the carrier of (LinearTopSpaceNorm X)
the U9 of (LinearTopSpaceNorm X) is V16() V19([:REAL, the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([:REAL, the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]
[:REAL, the carrier of (LinearTopSpaceNorm X):] is set
[:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is set
bool [:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
K175( the U9 of (LinearTopSpaceNorm X),f,G) is set
1 - f is complex real ext-real Element of REAL
(1 - f) * f is Element of the carrier of (LinearTopSpaceNorm X)
K175( the U9 of (LinearTopSpaceNorm X),(1 - f),f) is set
(f * G) + ((1 - f) * f) is Element of the carrier of (LinearTopSpaceNorm X)
the U7 of (LinearTopSpaceNorm X) is non empty V16() V19([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]
[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):] is non empty set
[:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
K179( the carrier of (LinearTopSpaceNorm X), the U7 of (LinearTopSpaceNorm X),(f * G),((1 - f) * f)) is Element of the carrier of (LinearTopSpaceNorm X)
n0 is Element of the carrier of X
f * n0 is Element of the carrier of X
the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is set
[:[:REAL, the carrier of X:], the carrier of X:] is set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K175( the U9 of X,f,n0) is set
r is Element of the carrier of X
(1 - f) * r is Element of the carrier of X
K175( the U9 of X,(1 - f),r) is set
(f * n0) + ((1 - f) * r) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,(f * n0),((1 - f) * r)) is Element of the carrier of X
X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of X is non empty set
Y is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
LinearTopSpaceNorm Y is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()
the carrier of (LinearTopSpaceNorm Y) is non empty set
bool the carrier of (LinearTopSpaceNorm Y) is non empty set
T is Element of the carrier of X
T1 is complex real ext-real set
Ball (T,T1) is Element of bool the carrier of X
bool the carrier of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : not T1 <= ||.(T - b₁).|| } is set
TB1 is non empty V16() V19( the carrier of X) V20( the carrier of Y) Function-like V26( the carrier of X) quasi_total V231(X,Y) V232(X,Y) Element of bool [: the carrier of X, the carrier of Y:]
TB1 .: (Ball (T,T1)) is Element of bool the carrier of Y
bool the carrier of Y is non empty set
G is Element of bool the carrier of (LinearTopSpaceNorm Y)
f is Element of bool the carrier of Y
LinearTopSpaceNorm X is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()
the carrier of (LinearTopSpaceNorm X) is non empty set
bool the carrier of (LinearTopSpaceNorm X) is non empty set
n0 is Element of the carrier of Y
r is Element of the carrier of Y
y0 is complex real ext-real Element of REAL
y0 * n0 is Element of the carrier of Y
the U9 of Y is V16() V19([:REAL, the carrier of Y:]) V20( the carrier of Y) Function-like V26([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is set
[:[:REAL, the carrier of Y:], the carrier of Y:] is set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
K175( the U9 of Y,y0,n0) is set
1 - y0 is complex real ext-real Element of REAL
(1 - y0) * r is Element of the carrier of Y
K175( the U9 of Y,(1 - y0),r) is set
(y0 * n0) + ((1 - y0) * r) is Element of the carrier of Y
the U7 of Y is non empty V16() V19([: the carrier of Y, the carrier of Y:]) V20( the carrier of Y) Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K179( the carrier of Y, the U7 of Y,(y0 * n0),((1 - y0) * r)) is Element of the carrier of Y
TBn0 is set
TB1 . TBn0 is set
TBn01 is Element of the carrier of X
yy0 is set
TB1 . yy0 is set
nb1 is Element of the carrier of X
(1 - y0) * nb1 is Element of the carrier of X
the U9 of X is V16() V19([:REAL, the carrier of X:]) V20( the carrier of X) Function-like V26([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]
[:REAL, the carrier of X:] is set
[:[:REAL, the carrier of X:], the carrier of X:] is set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K175( the U9 of X,(1 - y0),nb1) is set
TB1 . ((1 - y0) * nb1) is Element of the carrier of Y
LTBn01 is Element of the carrier of (LinearTopSpaceNorm X)
y0 * LTBn01 is Element of the carrier of (LinearTopSpaceNorm X)
the U9 of (LinearTopSpaceNorm X) is V16() V19([:REAL, the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([:REAL, the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]
[:REAL, the carrier of (LinearTopSpaceNorm X):] is set
[:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is set
bool [:[:REAL, the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
K175( the U9 of (LinearTopSpaceNorm X),y0,LTBn01) is set
y0 * TBn01 is Element of the carrier of X
K175( the U9 of X,y0,TBn01) is set
TBX1 is Element of the carrier of (LinearTopSpaceNorm X)
(1 - y0) * TBX1 is Element of the carrier of (LinearTopSpaceNorm X)
K175( the U9 of (LinearTopSpaceNorm X),(1 - y0),TBX1) is set
(y0 * LTBn01) + ((1 - y0) * TBX1) is Element of the carrier of (LinearTopSpaceNorm X)
the U7 of (LinearTopSpaceNorm X) is non empty V16() V19([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) V20( the carrier of (LinearTopSpaceNorm X)) Function-like V26([: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):]) quasi_total Element of bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):]
[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):] is non empty set
[:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
bool [:[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm X):], the carrier of (LinearTopSpaceNorm X):] is non empty set
K179( the carrier of (LinearTopSpaceNorm X), the U7 of (LinearTopSpaceNorm X),(y0 * LTBn01),((1 - y0) * TBX1)) is Element of the carrier of (LinearTopSpaceNorm X)
(y0 * TBn01) + ((1 - y0) * nb1) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,(y0 * TBn01),((1 - y0) * nb1)) is Element of the carrier of X
TB1 . (y0 * TBn01) is Element of the carrier of Y
TB1 . ((y0 * TBn01) + ((1 - y0) * nb1)) is Element of the carrier of Y
f is Element of bool the carrier of (LinearTopSpaceNorm X)
f is Element of the carrier of (LinearTopSpaceNorm Y)
n0 is Element of the carrier of (LinearTopSpaceNorm Y)
r is complex real ext-real Element of REAL
r * f is Element of the carrier of (LinearTopSpaceNorm Y)
the U9 of (LinearTopSpaceNorm Y) is V16() V19([:REAL, the carrier of (LinearTopSpaceNorm Y):]) V20( the carrier of (LinearTopSpaceNorm Y)) Function-like V26([:REAL, the carrier of (LinearTopSpaceNorm Y):]) quasi_total Element of bool [:[:REAL, the carrier of (LinearTopSpaceNorm Y):], the carrier of (LinearTopSpaceNorm Y):]
[:REAL, the carrier of (LinearTopSpaceNorm Y):] is set
[:[:REAL, the carrier of (LinearTopSpaceNorm Y):], the carrier of (LinearTopSpaceNorm Y):] is set
bool [:[:REAL, the carrier of (LinearTopSpaceNorm Y):], the carrier of (LinearTopSpaceNorm Y):] is non empty set
K175( the U9 of (LinearTopSpaceNorm Y),r,f) is set
1 - r is complex real ext-real Element of REAL
(1 - r) * n0 is Element of the carrier of (LinearTopSpaceNorm Y)
K175( the U9 of (LinearTopSpaceNorm Y),(1 - r),n0) is set
(r * f) + ((1 - r) * n0) is Element of the carrier of (LinearTopSpaceNorm Y)
the U7 of (LinearTopSpaceNorm Y) is non empty V16() V19([: the carrier of (LinearTopSpaceNorm Y), the carrier of (LinearTopSpaceNorm Y):]) V20( the carrier of (LinearTopSpaceNorm Y)) Function-like V26([: the carrier of (LinearTopSpaceNorm Y), the carrier of (LinearTopSpaceNorm Y):]) quasi_total Element of bool [:[: the carrier of (LinearTopSpaceNorm Y), the carrier of (LinearTopSpaceNorm Y):], the carrier of (LinearTopSpaceNorm Y):]
[: the carrier of (LinearTopSpaceNorm Y), the carrier of (LinearTopSpaceNorm Y):] is non empty set
[:[: the carrier of (LinearTopSpaceNorm Y), the carrier of (LinearTopSpaceNorm Y):], the carrier of (LinearTopSpaceNorm Y):] is non empty set
bool [:[: the carrier of (LinearTopSpaceNorm Y), the carrier of (LinearTopSpaceNorm Y):], the carrier of (LinearTopSpaceNorm Y):] is non empty set
K179( the carrier of (LinearTopSpaceNorm Y), the U7 of (LinearTopSpaceNorm Y),(r * f),((1 - r) * n0)) is Element of the carrier of (LinearTopSpaceNorm Y)
y0 is Element of the carrier of Y
r * y0 is Element of the carrier of Y
the U9 of Y is V16() V19([:REAL, the carrier of Y:]) V20( the carrier of Y) Function-like V26([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is set
[:[:REAL, the carrier of Y:], the carrier of Y:] is set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
K175( the U9 of Y,r,y0) is set
TBn0 is Element of the carrier of Y
(1 - r) * TBn0 is Element of the carrier of Y
K175( the U9 of Y,(1 - r),TBn0) is set
(r * y0) + ((1 - r) * TBn0) is Element of the carrier of Y
the U7 of Y is non empty V16() V19([: the carrier of Y, the carrier of Y:]) V20( the carrier of Y) Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K179( the carrier of Y, the U7 of Y,(r * y0),((1 - r) * TBn0)) is Element of the carrier of Y
X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of X is non empty set
Y is Element of the carrier of X
T is complex real ext-real set
T1 is complex real ext-real set
Ball (Y,T) is Element of bool the carrier of X
bool the carrier of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : not T <= ||.(Y - b₁).|| } is set
Ball (Y,T1) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not T1 <= ||.(Y - b₁).|| } is set
TB1 is Element of the carrier of X
T + T1 is complex real ext-real set
Y - TB1 is Element of the carrier of X
- TB1 is Element of the carrier of X
K230(X,Y,(- TB1)) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,Y,(- TB1)) is Element of the carrier of X
||.(Y - TB1).|| is complex real ext-real non negative Element of REAL
||.(Y - TB1).|| + T is complex real ext-real Element of REAL
G is Element of the carrier of X
Y - G is Element of the carrier of X
- G is Element of the carrier of X
K230(X,Y,(- G)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,Y,(- G)) is Element of the carrier of X
||.(Y - G).|| is complex real ext-real non negative Element of REAL
(T + T1) - T is complex real ext-real set
X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like V234() NORMSTR
the carrier of X is non empty set
LinearTopSpaceNorm X is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()
the carrier of (LinearTopSpaceNorm X) is non empty set
bool the carrier of (LinearTopSpaceNorm X) is non empty set
0. X is zero Element of the carrier of X
Ball ((0. X),1) is Element of bool the carrier of X
bool the carrier of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : not 1 <= ||.((0. X) - b₁).|| } is set
Y is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like NORMSTR
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
LinearTopSpaceNorm Y is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()
the carrier of (LinearTopSpaceNorm Y) is non empty set
bool the carrier of (LinearTopSpaceNorm Y) is non empty set
0. Y is zero Element of the carrier of Y
T is non empty V16() V19( the carrier of X) V20( the carrier of Y) Function-like V26( the carrier of X) quasi_total V231(X,Y) V232(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:]
T .: (Ball ((0. X),1)) is Element of bool the carrier of Y
bool the carrier of Y is non empty set
T1 is complex real ext-real set
Ball ((0. Y),T1) is Element of bool the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : not T1 <= ||.((0. Y) - b₁).|| } is set
f is Element of bool the carrier of (LinearTopSpaceNorm Y)
G is Element of bool the carrier of (LinearTopSpaceNorm Y)
Cl G is closed Element of bool the carrier of (LinearTopSpaceNorm Y)
n0 is Element of the carrier of X
T . n0 is Element of the carrier of Y
r is Element of the carrier of Y
y0 is Element of bool the carrier of (LinearTopSpaceNorm Y)
TBn0 is Element of bool the carrier of (LinearTopSpaceNorm Y)
Cl y0 is closed Element of bool the carrier of (LinearTopSpaceNorm Y)
TBn01 is complex real ext-real set
Ball (n0,TBn01) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not TBn01 <= ||.(n0 - b₁).|| } is set
T .: (Ball (n0,TBn01)) is Element of bool the carrier of Y
TBn01 * T1 is complex real ext-real set
Ball (r,(TBn01 * T1)) is Element of bool the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : not TBn01 * T1 <= ||.(r - b₁).|| } is set
Ball ((0. Y),(TBn01 * T1)) is Element of bool the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : not TBn01 * T1 <= ||.((0. Y) - b₁).|| } is set
r + (Ball ((0. Y),(TBn01 * T1))) is Element of bool the carrier of Y
{ K230(Y,r,b₁) where b₁ is Element of the carrier of Y : b₁ in Ball ((0. Y),(TBn01 * T1)) } is set
Ball ((0. X),TBn01) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not TBn01 <= ||.((0. X) - b₁).|| } is set
T .: (Ball ((0. X),TBn01)) is Element of bool the carrier of Y
n0 + (Ball ((0. X),TBn01)) is Element of bool the carrier of X
{ K230(X,n0,b₁) where b₁ is Element of the carrier of X : b₁ in Ball ((0. X),TBn01) } is set
TBX1 is Element of bool the carrier of Y
r + TBX1 is Element of bool the carrier of Y
{ K230(Y,r,b₁) where b₁ is Element of the carrier of Y : b₁ in TBX1 } is set
nb1 is Element of bool the carrier of Y
LTBn01 is non empty complex real ext-real Element of REAL
LTBn01 * f is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ (LTBn01 * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in f } is set
LTBn01 * (Cl G) is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ (LTBn01 * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in Cl G } is set
LTBn01 * G is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ (LTBn01 * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in G } is set
Cl (LTBn01 * G) is closed Element of bool the carrier of (LinearTopSpaceNorm Y)
yy0 is Element of the carrier of (LinearTopSpaceNorm Y)
yy0 + (LTBn01 * f) is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ K230((LinearTopSpaceNorm Y),yy0,b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in LTBn01 * f } is set
yy0 + (Cl (LTBn01 * G)) is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ K230((LinearTopSpaceNorm Y),yy0,b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in Cl (LTBn01 * G) } is set
yy0 + (LTBn01 * G) is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ K230((LinearTopSpaceNorm Y),yy0,b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in LTBn01 * G } is set
Cl (yy0 + (LTBn01 * G)) is closed Element of bool the carrier of (LinearTopSpaceNorm Y)
LTBn01 * (Ball ((0. Y),T1)) is Element of bool the carrier of Y
{ (LTBn01 * b₁) where b₁ is Element of the carrier of Y : b₁ in Ball ((0. Y),T1) } is set
LTBn01 * (Ball ((0. X),1)) is Element of bool the carrier of X
{ (LTBn01 * b₁) where b₁ is Element of the carrier of X : b₁ in Ball ((0. X),1) } is set
LTBn01 * 1 is complex real ext-real Element of REAL
Ball ((0. X),(LTBn01 * 1)) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not LTBn01 * 1 <= ||.((0. X) - b₁).|| } is set
f is Element of bool the carrier of Y
LTBn01 * f is Element of bool the carrier of Y
{ (LTBn01 * b₁) where b₁ is Element of the carrier of Y : b₁ in f } is set
f is complex real ext-real set
1 + f is complex real ext-real Element of REAL
Ball ((0. X),(1 + f)) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not 1 + f <= ||.((0. X) - b₁).|| } is set
T .: (Ball ((0. X),(1 + f))) is Element of bool the carrier of Y
n0 is set
y0 is complex real ext-real set
1 + y0 is complex real ext-real Element of REAL
y0 / (1 + y0) is complex real ext-real Element of REAL
(y0 / (1 + y0)) GeoSeq is V16() V19( NAT ) V20( REAL ) Function-like quasi_total Element of bool [:NAT,REAL:]
abs (y0 / (1 + y0)) is complex real ext-real Element of REAL
r is Element of the carrier of Y
((y0 / (1 + y0)) GeoSeq) . 1 is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . 1) * T1 is complex real ext-real Element of REAL
Ball (r,((((y0 / (1 + y0)) GeoSeq) . 1) * T1)) is Element of bool the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : not (((y0 / (1 + y0)) GeoSeq) . 1) * T1 <= ||.(r - b₁).|| } is set
(y0 / (1 + y0)) |^ 1 is complex real ext-real Element of REAL
r - r is Element of the carrier of Y
- r is Element of the carrier of Y
K230(Y,r,(- r)) is Element of the carrier of Y
the U7 of Y is non empty V16() V19([: the carrier of Y, the carrier of Y:]) V20( the carrier of Y) Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K179( the carrier of Y, the U7 of Y,r,(- r)) is Element of the carrier of Y
||.(r - r).|| is complex real ext-real non negative Element of REAL
LTBn01 is Element of bool the carrier of (LinearTopSpaceNorm Y)
yy0 is set
nb1 is set
T . nb1 is set
my0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
((y0 / (1 + y0)) GeoSeq) . my0 is complex real ext-real Element of REAL
my0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
((y0 / (1 + y0)) GeoSeq) . (my0 + 1) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . (my0 + 1)) * T1 is complex real ext-real Element of REAL
my0 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
((y0 / (1 + y0)) GeoSeq) . (my0 + 2) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . (my0 + 2)) * T1 is complex real ext-real Element of REAL
TBnx01 is Element of the carrier of X
BYyr is Element of the carrier of X
Ball (TBnx01,(((y0 / (1 + y0)) GeoSeq) . my0)) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not ((y0 / (1 + y0)) GeoSeq) . my0 <= ||.(TBnx01 - b₁).|| } is set
T . BYyr is Element of the carrier of Y
(T . BYyr) - r is Element of the carrier of Y
K230(Y,(T . BYyr),(- r)) is Element of the carrier of Y
K179( the carrier of Y, the U7 of Y,(T . BYyr),(- r)) is Element of the carrier of Y
||.((T . BYyr) - r).|| is complex real ext-real non negative Element of REAL
Ball (BYyr,(((y0 / (1 + y0)) GeoSeq) . (my0 + 1))) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not ((y0 / (1 + y0)) GeoSeq) . (my0 + 1) <= ||.(BYyr - b₁).|| } is set
Ball (r,((((y0 / (1 + y0)) GeoSeq) . (my0 + 2)) * T1)) is Element of bool the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : not (((y0 / (1 + y0)) GeoSeq) . (my0 + 2)) * T1 <= ||.(r - b₁).|| } is set
Ball ((T . BYyr),((((y0 / (1 + y0)) GeoSeq) . (my0 + 1)) * T1)) is Element of bool the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : not (((y0 / (1 + y0)) GeoSeq) . (my0 + 1)) * T1 <= ||.((T . BYyr) - b₁).|| } is set
T .: (Ball (BYyr,(((y0 / (1 + y0)) GeoSeq) . (my0 + 1)))) is Element of bool the carrier of Y
(y0 / (1 + y0)) |^ (my0 + 1) is complex real ext-real Element of REAL
XTB01 is Element of bool the carrier of (LinearTopSpaceNorm Y)
y is Element of bool the carrier of (LinearTopSpaceNorm Y)
Cl y is closed Element of bool the carrier of (LinearTopSpaceNorm Y)
(y0 / (1 + y0)) |^ (my0 + 2) is complex real ext-real Element of REAL
BYr is Element of bool the carrier of (LinearTopSpaceNorm Y)
x is set
p is set
T . p is set
TBp is Element of the carrier of X
T . TBp is Element of the carrier of Y
q is Element of the carrier of Y
(T . TBp) - r is Element of the carrier of Y
K230(Y,(T . TBp),(- r)) is Element of the carrier of Y
K179( the carrier of Y, the U7 of Y,(T . TBp),(- r)) is Element of the carrier of Y
||.((T . TBp) - r).|| is complex real ext-real non negative Element of REAL
q is Element of the carrier of Y
r - q is Element of the carrier of Y
- q is Element of the carrier of Y
K230(Y,r,(- q)) is Element of the carrier of Y
K179( the carrier of Y, the U7 of Y,r,(- q)) is Element of the carrier of Y
||.(r - q).|| is complex real ext-real non negative Element of REAL
BYr is Element of the carrier of X
T . BYr is Element of the carrier of Y
(T . BYr) - r is Element of the carrier of Y
K230(Y,(T . BYr),(- r)) is Element of the carrier of Y
K179( the carrier of Y, the U7 of Y,(T . BYr),(- r)) is Element of the carrier of Y
||.((T . BYr) - r).|| is complex real ext-real non negative Element of REAL
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
TBX1 is Element of the carrier of X
my0 is non empty V16() V19( NAT ) V20( the carrier of X) Function-like V26( NAT ) quasi_total Element of bool [:NAT, the carrier of X:]
my0 . 0 is Element of the carrier of X
my0 . 1 is Element of the carrier of X
T . TBX1 is Element of the carrier of Y
TBnx01 is Element of the carrier of Y
BYyr is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
BYyr + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
my0 . (BYyr + 1) is Element of the carrier of X
my0 . BYyr is Element of the carrier of X
((y0 / (1 + y0)) GeoSeq) . BYyr is complex real ext-real Element of REAL
Ball ((my0 . BYyr),(((y0 / (1 + y0)) GeoSeq) . BYyr)) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not ((y0 / (1 + y0)) GeoSeq) . BYyr <= ||.((my0 . BYyr) - b₁).|| } is set
((y0 / (1 + y0)) GeoSeq) . (BYyr + 1) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . (BYyr + 1)) * T1 is complex real ext-real Element of REAL
T . (my0 . (BYyr + 1)) is Element of the carrier of Y
(T . (my0 . (BYyr + 1))) - r is Element of the carrier of Y
K230(Y,(T . (my0 . (BYyr + 1))),(- r)) is Element of the carrier of Y
K179( the carrier of Y, the U7 of Y,(T . (my0 . (BYyr + 1))),(- r)) is Element of the carrier of Y
||.((T . (my0 . (BYyr + 1))) - r).|| is complex real ext-real non negative Element of REAL
BYyr + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
my0 . (BYyr + 2) is Element of the carrier of X
Ball ((my0 . (BYyr + 1)),(((y0 / (1 + y0)) GeoSeq) . (BYyr + 1))) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not ((y0 / (1 + y0)) GeoSeq) . (BYyr + 1) <= ||.((my0 . (BYyr + 1)) - b₁).|| } is set
((y0 / (1 + y0)) GeoSeq) . (BYyr + 2) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . (BYyr + 2)) * T1 is complex real ext-real Element of REAL
T . (my0 . (BYyr + 2)) is Element of the carrier of Y
(T . (my0 . (BYyr + 2))) - r is Element of the carrier of Y
K230(Y,(T . (my0 . (BYyr + 2))),(- r)) is Element of the carrier of Y
K179( the carrier of Y, the U7 of Y,(T . (my0 . (BYyr + 2))),(- r)) is Element of the carrier of Y
||.((T . (my0 . (BYyr + 2))) - r).|| is complex real ext-real non negative Element of REAL
(BYyr + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
my0 . ((BYyr + 1) + 1) is Element of the carrier of X
((y0 / (1 + y0)) GeoSeq) . ((BYyr + 1) + 1) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . ((BYyr + 1) + 1)) * T1 is complex real ext-real Element of REAL
T . (my0 . ((BYyr + 1) + 1)) is Element of the carrier of Y
(T . (my0 . ((BYyr + 1) + 1))) - r is Element of the carrier of Y
K230(Y,(T . (my0 . ((BYyr + 1) + 1))),(- r)) is Element of the carrier of Y
K179( the carrier of Y, the U7 of Y,(T . (my0 . ((BYyr + 1) + 1))),(- r)) is Element of the carrier of Y
||.((T . (my0 . ((BYyr + 1) + 1))) - r).|| is complex real ext-real non negative Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
my0 . (0 + 1) is Element of the carrier of X
((y0 / (1 + y0)) GeoSeq) . 0 is complex real ext-real Element of REAL
Ball ((my0 . 0),(((y0 / (1 + y0)) GeoSeq) . 0)) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not ((y0 / (1 + y0)) GeoSeq) . 0 <= ||.((my0 . 0) - b₁).|| } is set
((y0 / (1 + y0)) GeoSeq) . (0 + 1) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . (0 + 1)) * T1 is complex real ext-real Element of REAL
T . (my0 . (0 + 1)) is Element of the carrier of Y
(T . (my0 . (0 + 1))) - r is Element of the carrier of Y
K230(Y,(T . (my0 . (0 + 1))),(- r)) is Element of the carrier of Y
K179( the carrier of Y, the U7 of Y,(T . (my0 . (0 + 1))),(- r)) is Element of the carrier of Y
||.((T . (my0 . (0 + 1))) - r).|| is complex real ext-real non negative Element of REAL
BYyr is Element of the carrier of Y
r - BYyr is Element of the carrier of Y
- BYyr is Element of the carrier of Y
K230(Y,r,(- BYyr)) is Element of the carrier of Y
K179( the carrier of Y, the U7 of Y,r,(- BYyr)) is Element of the carrier of Y
||.(r - BYyr).|| is complex real ext-real non negative Element of REAL
((y0 / (1 + y0)) GeoSeq) . 0 is complex real ext-real Element of REAL
1 - (((y0 / (1 + y0)) GeoSeq) . 1) is complex real ext-real Element of REAL
BYyr is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
my0 . BYyr is Element of the carrier of X
((y0 / (1 + y0)) GeoSeq) . BYyr is complex real ext-real Element of REAL
BYr is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
(y0 / (1 + y0)) |^ BYr is complex real ext-real Element of REAL
BYr + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
(y0 / (1 + y0)) |^ (BYr + 1) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ BYr) - ((y0 / (1 + y0)) |^ (BYr + 1)) is complex real ext-real Element of REAL
1 - ((y0 / (1 + y0)) |^ 1) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) |^ BYr) - ((y0 / (1 + y0)) |^ (BYr + 1))) / (1 - ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
1 - ((y0 / (1 + y0)) |^ BYr) is complex real ext-real Element of REAL
(1 - ((y0 / (1 + y0)) |^ BYr)) / (1 - ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
((((y0 / (1 + y0)) |^ BYr) - ((y0 / (1 + y0)) |^ (BYr + 1))) / (1 - ((y0 / (1 + y0)) |^ 1))) + ((1 - ((y0 / (1 + y0)) |^ BYr)) / (1 - ((y0 / (1 + y0)) |^ 1))) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) |^ BYr) - ((y0 / (1 + y0)) |^ (BYr + 1))) + (1 - ((y0 / (1 + y0)) |^ BYr)) is complex real ext-real Element of REAL
((((y0 / (1 + y0)) |^ BYr) - ((y0 / (1 + y0)) |^ (BYr + 1))) + (1 - ((y0 / (1 + y0)) |^ BYr))) / (1 - ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
1 - ((y0 / (1 + y0)) |^ (BYr + 1)) is complex real ext-real Element of REAL
(1 - ((y0 / (1 + y0)) |^ (BYr + 1))) / (1 - ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
BYyr + BYr is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
my0 . (BYyr + BYr) is Element of the carrier of X
(my0 . (BYyr + BYr)) - (my0 . BYyr) is Element of the carrier of X
- (my0 . BYyr) is Element of the carrier of X
K230(X,(my0 . (BYyr + BYr)),(- (my0 . BYyr))) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,(my0 . (BYyr + BYr)),(- (my0 . BYyr))) is Element of the carrier of X
||.((my0 . (BYyr + BYr)) - (my0 . BYyr)).|| is complex real ext-real non negative Element of REAL
((y0 / (1 + y0)) GeoSeq) . BYr is complex real ext-real Element of REAL
1 - (((y0 / (1 + y0)) GeoSeq) . BYr) is complex real ext-real Element of REAL
(1 - (((y0 / (1 + y0)) GeoSeq) . BYr)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1)) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . BYyr) * ((1 - (((y0 / (1 + y0)) GeoSeq) . BYr)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1))) is complex real ext-real Element of REAL
(BYyr + BYr) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
my0 . ((BYyr + BYr) + 1) is Element of the carrier of X
(my0 . ((BYyr + BYr) + 1)) - (my0 . BYyr) is Element of the carrier of X
K230(X,(my0 . ((BYyr + BYr) + 1)),(- (my0 . BYyr))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(my0 . ((BYyr + BYr) + 1)),(- (my0 . BYyr))) is Element of the carrier of X
||.((my0 . ((BYyr + BYr) + 1)) - (my0 . BYyr)).|| is complex real ext-real non negative Element of REAL
(my0 . ((BYyr + BYr) + 1)) - (my0 . (BYyr + BYr)) is Element of the carrier of X
- (my0 . (BYyr + BYr)) is Element of the carrier of X
K230(X,(my0 . ((BYyr + BYr) + 1)),(- (my0 . (BYyr + BYr)))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(my0 . ((BYyr + BYr) + 1)),(- (my0 . (BYyr + BYr)))) is Element of the carrier of X
||.((my0 . ((BYyr + BYr) + 1)) - (my0 . (BYyr + BYr))).|| is complex real ext-real non negative Element of REAL
||.((my0 . ((BYyr + BYr) + 1)) - (my0 . (BYyr + BYr))).|| + ||.((my0 . (BYyr + BYr)) - (my0 . BYyr)).|| is complex real ext-real non negative Element of REAL
||.((my0 . ((BYyr + BYr) + 1)) - (my0 . (BYyr + BYr))).|| + ((((y0 / (1 + y0)) GeoSeq) . BYyr) * ((1 - (((y0 / (1 + y0)) GeoSeq) . BYr)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1)))) is complex real ext-real Element of REAL
BYyr + (BYr + 1) is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
my0 . (BYyr + (BYr + 1)) is Element of the carrier of X
(my0 . (BYyr + (BYr + 1))) - (my0 . BYyr) is Element of the carrier of X
K230(X,(my0 . (BYyr + (BYr + 1))),(- (my0 . BYyr))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(my0 . (BYyr + (BYr + 1))),(- (my0 . BYyr))) is Element of the carrier of X
||.((my0 . (BYyr + (BYr + 1))) - (my0 . BYyr)).|| is complex real ext-real non negative Element of REAL
((y0 / (1 + y0)) GeoSeq) . (BYyr + BYr) is complex real ext-real Element of REAL
Ball ((my0 . (BYyr + BYr)),(((y0 / (1 + y0)) GeoSeq) . (BYyr + BYr))) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not ((y0 / (1 + y0)) GeoSeq) . (BYyr + BYr) <= ||.((my0 . (BYyr + BYr)) - b₁).|| } is set
XTB01 is Element of the carrier of X
(my0 . (BYyr + BYr)) - XTB01 is Element of the carrier of X
- XTB01 is Element of the carrier of X
K230(X,(my0 . (BYyr + BYr)),(- XTB01)) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(my0 . (BYyr + BYr)),(- XTB01)) is Element of the carrier of X
||.((my0 . (BYyr + BYr)) - XTB01).|| is complex real ext-real non negative Element of REAL
(((y0 / (1 + y0)) GeoSeq) . (BYyr + BYr)) + ((((y0 / (1 + y0)) GeoSeq) . BYyr) * ((1 - (((y0 / (1 + y0)) GeoSeq) . BYr)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1)))) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ BYr) * (1 - ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) |^ BYr) * (1 - ((y0 / (1 + y0)) |^ 1))) / (1 - ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ BYr) * ((y0 / (1 + y0)) |^ 1) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ BYr) - (((y0 / (1 + y0)) |^ BYr) * ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) |^ BYr) - (((y0 / (1 + y0)) |^ BYr) * ((y0 / (1 + y0)) |^ 1))) / (1 - ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
(y0 / (1 + y0)) |^ (BYyr + BYr) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ (BYyr + BYr)) + ((((y0 / (1 + y0)) GeoSeq) . BYyr) * ((1 - (((y0 / (1 + y0)) GeoSeq) . BYr)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1)))) is complex real ext-real Element of REAL
(y0 / (1 + y0)) |^ BYyr is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ BYyr) * ((1 - (((y0 / (1 + y0)) GeoSeq) . BYr)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1))) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ (BYyr + BYr)) + (((y0 / (1 + y0)) |^ BYyr) * ((1 - (((y0 / (1 + y0)) GeoSeq) . BYr)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1)))) is complex real ext-real Element of REAL
(1 - ((y0 / (1 + y0)) |^ BYr)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1)) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ BYyr) * ((1 - ((y0 / (1 + y0)) |^ BYr)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1))) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ (BYyr + BYr)) + (((y0 / (1 + y0)) |^ BYyr) * ((1 - ((y0 / (1 + y0)) |^ BYr)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1)))) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ BYyr) * ((1 - ((y0 / (1 + y0)) |^ BYr)) / (1 - ((y0 / (1 + y0)) |^ 1))) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ (BYyr + BYr)) + (((y0 / (1 + y0)) |^ BYyr) * ((1 - ((y0 / (1 + y0)) |^ BYr)) / (1 - ((y0 / (1 + y0)) |^ 1)))) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ BYyr) * ((y0 / (1 + y0)) |^ BYr) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) |^ BYyr) * ((y0 / (1 + y0)) |^ BYr)) + (((y0 / (1 + y0)) |^ BYyr) * ((1 - ((y0 / (1 + y0)) |^ BYr)) / (1 - ((y0 / (1 + y0)) |^ 1)))) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ BYyr) * ((1 - ((y0 / (1 + y0)) |^ (BYr + 1))) / (1 - ((y0 / (1 + y0)) |^ 1))) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . BYyr) * ((1 - ((y0 / (1 + y0)) |^ (BYr + 1))) / (1 - ((y0 / (1 + y0)) |^ 1))) is complex real ext-real Element of REAL
((y0 / (1 + y0)) GeoSeq) . (BYr + 1) is complex real ext-real Element of REAL
1 - (((y0 / (1 + y0)) GeoSeq) . (BYr + 1)) is complex real ext-real Element of REAL
(1 - (((y0 / (1 + y0)) GeoSeq) . (BYr + 1))) / (1 - ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . BYyr) * ((1 - (((y0 / (1 + y0)) GeoSeq) . (BYr + 1))) / (1 - ((y0 / (1 + y0)) |^ 1))) is complex real ext-real Element of REAL
(1 - (((y0 / (1 + y0)) GeoSeq) . (BYr + 1))) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1)) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . BYyr) * ((1 - (((y0 / (1 + y0)) GeoSeq) . (BYr + 1))) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1))) is complex real ext-real Element of REAL
BYyr + 0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
my0 . (BYyr + 0) is Element of the carrier of X
(my0 . (BYyr + 0)) - (my0 . BYyr) is Element of the carrier of X
K230(X,(my0 . (BYyr + 0)),(- (my0 . BYyr))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(my0 . (BYyr + 0)),(- (my0 . BYyr))) is Element of the carrier of X
||.((my0 . (BYyr + 0)) - (my0 . BYyr)).|| is complex real ext-real non negative Element of REAL
||.(0. X).|| is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative Element of REAL
1 - (((y0 / (1 + y0)) GeoSeq) . 0) is complex real ext-real Element of REAL
(1 - (((y0 / (1 + y0)) GeoSeq) . 0)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1)) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . BYyr) * ((1 - (((y0 / (1 + y0)) GeoSeq) . 0)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1))) is complex real ext-real Element of REAL
BYr is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
BYyr + BYr is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
my0 . (BYyr + BYr) is Element of the carrier of X
(my0 . (BYyr + BYr)) - (my0 . BYyr) is Element of the carrier of X
K230(X,(my0 . (BYyr + BYr)),(- (my0 . BYyr))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(my0 . (BYyr + BYr)),(- (my0 . BYyr))) is Element of the carrier of X
||.((my0 . (BYyr + BYr)) - (my0 . BYyr)).|| is complex real ext-real non negative Element of REAL
((y0 / (1 + y0)) GeoSeq) . BYr is complex real ext-real Element of REAL
1 - (((y0 / (1 + y0)) GeoSeq) . BYr) is complex real ext-real Element of REAL
(1 - (((y0 / (1 + y0)) GeoSeq) . BYr)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1)) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . BYyr) * ((1 - (((y0 / (1 + y0)) GeoSeq) . BYr)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1))) is complex real ext-real Element of REAL
||.my0.|| is V16() V19( NAT ) V20( REAL ) Function-like quasi_total Element of bool [:NAT,REAL:]
1 - (y0 / (1 + y0)) is complex real ext-real Element of REAL
1 / (1 - (y0 / (1 + y0))) is complex real ext-real Element of REAL
BYyr is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
||.my0.|| . BYyr is complex real ext-real Element of REAL
((y0 / (1 + y0)) GeoSeq) . BYyr is complex real ext-real Element of REAL
(y0 / (1 + y0)) |^ BYyr is complex real ext-real Element of REAL
1 - ((y0 / (1 + y0)) |^ 1) is complex real ext-real Element of REAL
1 - ((y0 / (1 + y0)) |^ BYyr) is complex real ext-real Element of REAL
1 - (((y0 / (1 + y0)) GeoSeq) . BYyr) is complex real ext-real Element of REAL
(1 - (((y0 / (1 + y0)) GeoSeq) . BYyr)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1)) is complex real ext-real Element of REAL
1 / (1 - ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
0 + BYyr is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
my0 . (0 + BYyr) is Element of the carrier of X
(my0 . (0 + BYyr)) - (my0 . 0) is Element of the carrier of X
- (my0 . 0) is Element of the carrier of X
K230(X,(my0 . (0 + BYyr)),(- (my0 . 0))) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,(my0 . (0 + BYyr)),(- (my0 . 0))) is Element of the carrier of X
||.((my0 . (0 + BYyr)) - (my0 . 0)).|| is complex real ext-real non negative Element of REAL
(((y0 / (1 + y0)) GeoSeq) . 0) * ((1 - (((y0 / (1 + y0)) GeoSeq) . BYyr)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1))) is complex real ext-real Element of REAL
my0 . BYyr is Element of the carrier of X
||.(my0 . BYyr).|| is complex real ext-real non negative Element of REAL
Sum ((y0 / (1 + y0)) GeoSeq) is complex real ext-real Element of REAL
1 * (1 + y0) is complex real ext-real Element of REAL
(1 * (1 + y0)) - y0 is complex real ext-real Element of REAL
((1 * (1 + y0)) - y0) / (1 + y0) is complex real ext-real Element of REAL
1 / (((1 * (1 + y0)) - y0) / (1 + y0)) is complex real ext-real Element of REAL
lim my0 is Element of the carrier of X
BYr is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
(y0 / (1 + y0)) |^ BYr is complex real ext-real Element of REAL
XTB01 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
BYr + XTB01 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
my0 . (BYr + XTB01) is Element of the carrier of X
my0 . BYr is Element of the carrier of X
(my0 . (BYr + XTB01)) - (my0 . BYr) is Element of the carrier of X
- (my0 . BYr) is Element of the carrier of X
K230(X,(my0 . (BYr + XTB01)),(- (my0 . BYr))) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,(my0 . (BYr + XTB01)),(- (my0 . BYr))) is Element of the carrier of X
||.((my0 . (BYr + XTB01)) - (my0 . BYr)).|| is complex real ext-real non negative Element of REAL
((y0 / (1 + y0)) GeoSeq) . BYr is complex real ext-real Element of REAL
((y0 / (1 + y0)) GeoSeq) . XTB01 is complex real ext-real Element of REAL
1 - (((y0 / (1 + y0)) GeoSeq) . XTB01) is complex real ext-real Element of REAL
(1 - (((y0 / (1 + y0)) GeoSeq) . XTB01)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1)) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . BYr) * ((1 - (((y0 / (1 + y0)) GeoSeq) . XTB01)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1))) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ BYr) * ((1 - (((y0 / (1 + y0)) GeoSeq) . XTB01)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1))) is complex real ext-real Element of REAL
(y0 / (1 + y0)) |^ XTB01 is complex real ext-real Element of REAL
1 - ((y0 / (1 + y0)) |^ XTB01) is complex real ext-real Element of REAL
(1 - ((y0 / (1 + y0)) |^ XTB01)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1)) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ BYr) * ((1 - ((y0 / (1 + y0)) |^ XTB01)) / (1 - (((y0 / (1 + y0)) GeoSeq) . 1))) is complex real ext-real Element of REAL
1 - ((y0 / (1 + y0)) |^ 1) is complex real ext-real Element of REAL
(1 - ((y0 / (1 + y0)) |^ XTB01)) / (1 - ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ BYr) * ((1 - ((y0 / (1 + y0)) |^ XTB01)) / (1 - ((y0 / (1 + y0)) |^ 1))) is complex real ext-real Element of REAL
1 / (1 - ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ BYr) * (1 / (1 - ((y0 / (1 + y0)) |^ 1))) is complex real ext-real Element of REAL
lim ((y0 / (1 + y0)) GeoSeq) is complex real ext-real Element of REAL
BYr is complex real ext-real Element of REAL
BYr * (1 - ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
XTB01 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
((y0 / (1 + y0)) GeoSeq) . XTB01 is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . XTB01) - 0 is complex real ext-real Element of REAL
abs ((((y0 / (1 + y0)) GeoSeq) . XTB01) - 0) is complex real ext-real Element of REAL
0 + (BYr * (1 - ((y0 / (1 + y0)) |^ 1))) is complex real ext-real Element of REAL
(BYr * (1 - ((y0 / (1 + y0)) |^ 1))) / (1 - ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . XTB01) / (1 - ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
(y0 / (1 + y0)) |^ XTB01 is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ XTB01) / (1 - ((y0 / (1 + y0)) |^ 1)) is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ XTB01) * (1 / (1 - ((y0 / (1 + y0)) |^ 1))) is complex real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
y + p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
TBp is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
y + TBp is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
my0 . x is Element of the carrier of X
my0 . y is Element of the carrier of X
(my0 . x) - (my0 . y) is Element of the carrier of X
- (my0 . y) is Element of the carrier of X
K230(X,(my0 . x),(- (my0 . y))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(my0 . x),(- (my0 . y))) is Element of the carrier of X
||.((my0 . x) - (my0 . y)).|| is complex real ext-real non negative Element of REAL
lim ||.my0.|| is complex real ext-real Element of REAL
||.(lim my0).|| is complex real ext-real non negative Element of REAL
- (lim my0) is Element of the carrier of X
||.(- (lim my0)).|| is complex real ext-real non negative Element of REAL
(0. X) - (lim my0) is Element of the carrier of X
K230(X,(0. X),(- (lim my0))) is Element of the carrier of X
K179( the carrier of X, the U7 of X,(0. X),(- (lim my0))) is Element of the carrier of X
||.((0. X) - (lim my0)).|| is complex real ext-real non negative Element of REAL
rng my0 is Element of bool the carrier of X
dom T is Element of bool the carrier of X
T /* my0 is non empty V16() V19( NAT ) V20( the carrier of Y) Function-like V26( NAT ) quasi_total Element of bool [:NAT, the carrier of Y:]
[:NAT, the carrier of Y:] is non empty set
bool [:NAT, the carrier of Y:] is non empty set
BYr is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
(T /* my0) . BYr is Element of the carrier of Y
my0 . BYr is Element of the carrier of X
T /. (my0 . BYr) is Element of the carrier of Y
T . (my0 . BYr) is Element of the carrier of Y
BYr is complex real ext-real Element of REAL
BYr / T1 is complex real ext-real Element of REAL
XTB01 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
XTB01 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
(y0 / (1 + y0)) |^ XTB01 is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ XTB01) * ((y0 / (1 + y0)) |^ 1) is complex real ext-real Element of REAL
(y0 / (1 + y0)) |^ (XTB01 + 1) is complex real ext-real Element of REAL
((y0 / (1 + y0)) GeoSeq) . (XTB01 + 1) is complex real ext-real Element of REAL
((y0 / (1 + y0)) GeoSeq) . XTB01 is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . XTB01) - 0 is complex real ext-real Element of REAL
abs ((((y0 / (1 + y0)) GeoSeq) . XTB01) - 0) is complex real ext-real Element of REAL
0 + (BYr / T1) is complex real ext-real Element of REAL
(BYr / T1) * T1 is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . (XTB01 + 1)) * T1 is complex real ext-real Element of REAL
y is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
x - 1 is complex real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
TBp is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative set
(XTB01 + 1) + TBp is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
(y0 / (1 + y0)) |^ (p + 1) is complex real ext-real Element of REAL
(y0 / (1 + y0)) |^ TBp is complex real ext-real Element of REAL
((y0 / (1 + y0)) |^ (XTB01 + 1)) * ((y0 / (1 + y0)) |^ TBp) is complex real ext-real Element of REAL
1 |^ TBp is complex real ext-real Element of REAL
((y0 / (1 + y0)) GeoSeq) . (p + 1) is complex real ext-real Element of REAL
(((y0 / (1 + y0)) GeoSeq) . (p + 1)) * T1 is complex real ext-real Element of REAL
my0 . x is Element of the carrier of X
T . (my0 . x) is Element of the carrier of Y
(T . (my0 . x)) - r is Element of the carrier of Y
K230(Y,(T . (my0 . x)),(- r)) is Element of the carrier of Y
K179( the carrier of Y, the U7 of Y,(T . (my0 . x)),(- r)) is Element of the carrier of Y
||.((T . (my0 . x)) - r).|| is complex real ext-real non negative Element of REAL
(T /* my0) . x is Element of the carrier of Y
((T /* my0) . x) - r is Element of the carrier of Y
K230(Y,((T /* my0) . x),(- r)) is Element of the carrier of Y
K179( the carrier of Y, the U7 of Y,((T /* my0) . x),(- r)) is Element of the carrier of Y
||.(((T /* my0) . x) - r).|| is complex real ext-real non negative Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
(T /* my0) . x is Element of the carrier of Y
((T /* my0) . x) - r is Element of the carrier of Y
K230(Y,((T /* my0) . x),(- r)) is Element of the carrier of Y
K179( the carrier of Y, the U7 of Y,((T /* my0) . x),(- r)) is Element of the carrier of Y
||.(((T /* my0) . x) - r).|| is complex real ext-real non negative Element of REAL
T /. (lim my0) is Element of the carrier of Y
T . (lim my0) is Element of the carrier of Y
lim (T /* my0) is Element of the carrier of Y
n0 is set
r is Element of the carrier of Y
- r is Element of the carrier of Y
||.(- r).|| is complex real ext-real non negative Element of REAL
y0 is Element of the carrier of Y
(0. Y) - y0 is Element of the carrier of Y
- y0 is Element of the carrier of Y
K230(Y,(0. Y),(- y0)) is Element of the carrier of Y
the U7 of Y is non empty V16() V19([: the carrier of Y, the carrier of Y:]) V20( the carrier of Y) Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K179( the carrier of Y, the U7 of Y,(0. Y),(- y0)) is Element of the carrier of Y
||.((0. Y) - y0).|| is complex real ext-real non negative Element of REAL
||.r.|| is complex real ext-real non negative Element of REAL
y0 is complex real ext-real set
1 + y0 is complex real ext-real Element of REAL
T1 / (1 + y0) is complex real ext-real Element of REAL
(1 + y0) * r is Element of the carrier of Y
the U9 of Y is V16() V19([:REAL, the carrier of Y:]) V20( the carrier of Y) Function-like V26([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is set
[:[:REAL, the carrier of Y:], the carrier of Y:] is set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
K175( the U9 of Y,(1 + y0),r) is set
(T1 / (1 + y0)) * (1 + y0) is complex real ext-real Element of REAL
(1 + y0) * ||.r.|| is complex real ext-real Element of REAL
abs (1 + y0) is complex real ext-real Element of REAL
(abs (1 + y0)) * ||.r.|| is complex real ext-real Element of REAL
||.((1 + y0) * r).|| is complex real ext-real non negative Element of REAL
- ((1 + y0) * r) is Element of the carrier of Y
||.(- ((1 + y0) * r)).|| is complex real ext-real non negative Element of REAL
(0. Y) - ((1 + y0) * r) is Element of the carrier of Y
K230(Y,(0. Y),(- ((1 + y0) * r))) is Element of the carrier of Y
the U7 of Y is non empty V16() V19([: the carrier of Y, the carrier of Y:]) V20( the carrier of Y) Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K179( the carrier of Y, the U7 of Y,(0. Y),(- ((1 + y0) * r))) is Element of the carrier of Y
||.((0. Y) - ((1 + y0) * r)).|| is complex real ext-real non negative Element of REAL
Ball ((0. X),(1 + y0)) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not 1 + y0 <= ||.((0. X) - b₁).|| } is set
T .: (Ball ((0. X),(1 + y0))) is Element of bool the carrier of Y
TBn01 is non empty complex real ext-real Element of REAL
TBn01 * (Ball ((0. X),1)) is Element of bool the carrier of X
{ (TBn01 * b₁) where b₁ is Element of the carrier of X : b₁ in Ball ((0. X),1) } is set
TBn01 * 1 is complex real ext-real Element of REAL
Ball ((0. X),(TBn01 * 1)) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not TBn01 * 1 <= ||.((0. X) - b₁).|| } is set
TBn01 * r is Element of the carrier of Y
K175( the U9 of Y,TBn01,r) is set
f is Element of bool the carrier of Y
TBn01 * f is Element of bool the carrier of Y
{ (TBn01 * b₁) where b₁ is Element of the carrier of Y : b₁ in f } is set
TBn01 " is complex real ext-real Element of REAL
(TBn01 ") * (TBn01 * r) is Element of the carrier of Y
K175( the U9 of Y,(TBn01 "),(TBn01 * r)) is set
(TBn01 ") * (TBn01 * f) is Element of bool the carrier of Y
{ ((TBn01 ") * b₁) where b₁ is Element of the carrier of Y : b₁ in TBn01 * f } is set
(TBn01 ") * TBn01 is complex real ext-real Element of REAL
((TBn01 ") * TBn01) * r is Element of the carrier of Y
K175( the U9 of Y,((TBn01 ") * TBn01),r) is set
((TBn01 ") * TBn01) * f is Element of bool the carrier of Y
{ (((TBn01 ") * TBn01) * b₁) where b₁ is Element of the carrier of Y : b₁ in f } is set
1 / TBn01 is complex real ext-real Element of REAL
(1 / TBn01) * TBn01 is complex real ext-real Element of REAL
1 * f is Element of bool the carrier of Y
{ (1 * b₁) where b₁ is Element of the carrier of Y : b₁ in f } is set
X is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like V234() NORMSTR
the carrier of X is non empty set
Y is non empty V113() V138() V139() V140() V141() V142() V143() V144() discerning V150() RealNormSpace-like V234() NORMSTR
the carrier of Y is non empty set
[: the carrier of X, the carrier of Y:] is non empty set
bool [: the carrier of X, the carrier of Y:] is non empty set
LinearTopSpaceNorm X is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()
the carrier of (LinearTopSpaceNorm X) is non empty set
LinearTopSpaceNorm Y is non empty TopSpace-like T_2 V113() V138() V139() V140() V141() V142() V143() V144() V205() V206() V207() L19()
the carrier of (LinearTopSpaceNorm Y) is non empty set
[: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm Y):] is non empty set
bool [: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm Y):] is non empty set
T is non empty V16() V19( the carrier of X) V20( the carrier of Y) Function-like V26( the carrier of X) quasi_total V231(X,Y) V232(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:]
T1 is non empty V16() V19( the carrier of (LinearTopSpaceNorm X)) V20( the carrier of (LinearTopSpaceNorm Y)) Function-like V26( the carrier of (LinearTopSpaceNorm X)) quasi_total Element of bool [: the carrier of (LinearTopSpaceNorm X), the carrier of (LinearTopSpaceNorm Y):]
bool the carrier of (LinearTopSpaceNorm X) is non empty set
bool the carrier of (LinearTopSpaceNorm Y) is non empty set
0. X is zero Element of the carrier of X
Ball ((0. X),1) is Element of bool the carrier of X
bool the carrier of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : not 1 <= ||.((0. X) - b₁).|| } is set
T .: (Ball ((0. X),1)) is Element of bool the carrier of Y
bool the carrier of Y is non empty set
TopSpaceNorm Y is non empty TopSpace-like TopStruct
MetricSpaceNorm Y is non empty V88() V89() V90() V91() L7()
distance_by_norm_of Y is V16() V19([: the carrier of Y, the carrier of Y:]) V20( REAL ) Function-like quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:],REAL:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:],REAL:] is set
bool [:[: the carrier of Y, the carrier of Y:],REAL:] is non empty set
G7( the carrier of Y,(distance_by_norm_of Y)) is V83() L7()
K210((MetricSpaceNorm Y)) is TopStruct
the carrier of (MetricSpaceNorm Y) is non empty set
K209((MetricSpaceNorm Y)) is Element of bool (bool the carrier of (MetricSpaceNorm Y))
bool the carrier of (MetricSpaceNorm Y) is non empty set
bool (bool the carrier of (MetricSpaceNorm Y)) is non empty set
TopStruct(# the carrier of (MetricSpaceNorm Y),K209((MetricSpaceNorm Y)) #) is strict TopStruct
the carrier of (TopSpaceNorm Y) is non empty set
bool the carrier of (TopSpaceNorm Y) is non empty set
G is Element of bool the carrier of (LinearTopSpaceNorm X)
T1 .: G is Element of bool the carrier of (LinearTopSpaceNorm Y)
f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
Ball ((0. X),f) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not f <= ||.((0. X) - b₁).|| } is set
T .: (Ball ((0. X),f)) is Element of bool the carrier of Y
f is Element of bool the carrier of (TopSpaceNorm Y)
Cl f is closed Element of bool the carrier of (TopSpaceNorm Y)
[:NAT,(bool the carrier of Y):] is non empty set
bool [:NAT,(bool the carrier of Y):] is non empty set
f is non empty V16() V19( NAT ) V20( bool the carrier of Y) Function-like V26( NAT ) quasi_total Element of bool [:NAT,(bool the carrier of Y):]
K558( the carrier of Y) is non empty Element of bool (bool the carrier of Y)
bool (bool the carrier of Y) is non empty set
[:NAT,K558( the carrier of Y):] is non empty set
bool [:NAT,K558( the carrier of Y):] is non empty set
f is non empty V16() V19( NAT ) V20(K558( the carrier of Y)) Function-like V26( NAT ) quasi_total Element of bool [:NAT,K558( the carrier of Y):]
n0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
f . n0 is Element of K558( the carrier of Y)
Ball ((0. X),n0) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not n0 <= ||.((0. X) - b₁).|| } is set
T .: (Ball ((0. X),n0)) is Element of bool the carrier of Y
r is Element of bool the carrier of (TopSpaceNorm Y)
Cl r is closed Element of bool the carrier of (TopSpaceNorm Y)
rng f is Element of bool K558( the carrier of Y)
bool K558( the carrier of Y) is non empty set
union (rng f) is set
n0 is set
rng T is Element of bool the carrier of Y
r is Element of the carrier of Y
y0 is set
T . y0 is set
TBn0 is Element of the carrier of X
||.TBn0.|| is complex real ext-real non negative Element of REAL
TBn01 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
TBn01 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
||.TBn0.|| + 0 is complex real ext-real non negative Element of REAL
- TBn0 is Element of the carrier of X
||.(- TBn0).|| is complex real ext-real non negative Element of REAL
(0. X) - TBn0 is Element of the carrier of X
K230(X,(0. X),(- TBn0)) is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,(0. X),(- TBn0)) is Element of the carrier of X
||.((0. X) - TBn0).|| is complex real ext-real non negative Element of REAL
Ball ((0. X),(TBn01 + 1)) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not TBn01 + 1 <= ||.((0. X) - b₁).|| } is set
T . TBn0 is Element of the carrier of Y
T .: (Ball ((0. X),(TBn01 + 1))) is Element of bool the carrier of Y
dom f is Element of bool NAT
f . (TBn01 + 1) is Element of K558( the carrier of Y)
yy0 is Element of bool the carrier of (TopSpaceNorm Y)
Cl yy0 is closed Element of bool the carrier of (TopSpaceNorm Y)
r is complex real ext-real Element of REAL
y0 is Element of the carrier of Y
Ball (y0,r) is Element of bool the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : not r <= ||.(y0 - b₁).|| } is set
n0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
f . n0 is Element of K558( the carrier of Y)
Ball ((0. X),n0) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not n0 <= ||.((0. X) - b₁).|| } is set
T .: (Ball ((0. X),n0)) is Element of bool the carrier of Y
TBn0 is Element of bool the carrier of (TopSpaceNorm Y)
Cl TBn0 is closed Element of bool the carrier of (TopSpaceNorm Y)
n0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
Ball ((0. X),(n0 + 1)) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not n0 + 1 <= ||.((0. X) - b₁).|| } is set
T .: (Ball ((0. X),(n0 + 1))) is Element of bool the carrier of Y
f . (n0 + 1) is Element of K558( the carrier of Y)
TBn01 is Element of bool the carrier of (TopSpaceNorm Y)
Cl TBn01 is closed Element of bool the carrier of (TopSpaceNorm Y)
LTBn01 is Element of bool the carrier of (LinearTopSpaceNorm Y)
(- 1) * LTBn01 is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ ((- 1) * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in LTBn01 } is set
Cl ((- 1) * LTBn01) is closed Element of bool the carrier of (LinearTopSpaceNorm Y)
Cl LTBn01 is closed Element of bool the carrier of (LinearTopSpaceNorm Y)
(- 1) * (Cl LTBn01) is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ ((- 1) * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in Cl LTBn01 } is set
0. Y is zero Element of the carrier of Y
2 * n0 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
(2 * n0) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
r / ((2 * n0) + 2) is complex real ext-real Element of REAL
Ball ((0. Y),(r / ((2 * n0) + 2))) is Element of bool the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : not r / ((2 * n0) + 2) <= ||.((0. Y) - b₁).|| } is set
y0 - y0 is Element of the carrier of Y
- y0 is Element of the carrier of Y
K230(Y,y0,(- y0)) is Element of the carrier of Y
the U7 of Y is non empty V16() V19([: the carrier of Y, the carrier of Y:]) V20( the carrier of Y) Function-like V26([: the carrier of Y, the carrier of Y:]) quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
K179( the carrier of Y, the U7 of Y,y0,(- y0)) is Element of the carrier of Y
||.(y0 - y0).|| is complex real ext-real non negative Element of REAL
yy0 is Element of the carrier of (LinearTopSpaceNorm Y)
(- 1) * yy0 is Element of the carrier of (LinearTopSpaceNorm Y)
the U9 of (LinearTopSpaceNorm Y) is V16() V19([:REAL, the carrier of (LinearTopSpaceNorm Y):]) V20( the carrier of (LinearTopSpaceNorm Y)) Function-like V26([:REAL, the carrier of (LinearTopSpaceNorm Y):]) quasi_total Element of bool [:[:REAL, the carrier of (LinearTopSpaceNorm Y):], the carrier of (LinearTopSpaceNorm Y):]
[:REAL, the carrier of (LinearTopSpaceNorm Y):] is set
[:[:REAL, the carrier of (LinearTopSpaceNorm Y):], the carrier of (LinearTopSpaceNorm Y):] is set
bool [:[:REAL, the carrier of (LinearTopSpaceNorm Y):], the carrier of (LinearTopSpaceNorm Y):] is non empty set
K175( the U9 of (LinearTopSpaceNorm Y),(- 1),yy0) is set
1 / ((2 * n0) + 2) is complex real ext-real non negative Element of REAL
- yy0 is Element of the carrier of (LinearTopSpaceNorm Y)
{(- yy0)} is Element of bool the carrier of (LinearTopSpaceNorm Y)
Ball ((0. Y),r) is Element of bool the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : not r <= ||.((0. Y) - b₁).|| } is set
(- 1) * y0 is Element of the carrier of Y
the U9 of Y is V16() V19([:REAL, the carrier of Y:]) V20( the carrier of Y) Function-like V26([:REAL, the carrier of Y:]) quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is set
[:[:REAL, the carrier of Y:], the carrier of Y:] is set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
K175( the U9 of Y,(- 1),y0) is set
XTB01 is Element of bool the carrier of Y
(- 1) * XTB01 is Element of bool the carrier of Y
{ ((- 1) * b₁) where b₁ is Element of the carrier of Y : b₁ in XTB01 } is set
(- 1) * (Ball ((0. X),(n0 + 1))) is Element of bool the carrier of X
{ ((- 1) * b₁) where b₁ is Element of the carrier of X : b₁ in Ball ((0. X),(n0 + 1)) } is set
T .: ((- 1) * (Ball ((0. X),(n0 + 1)))) is Element of bool the carrier of Y
my0 is Element of bool the carrier of (LinearTopSpaceNorm Y)
TBnx01 is Element of bool the carrier of (LinearTopSpaceNorm Y)
Cl TBnx01 is closed Element of bool the carrier of (LinearTopSpaceNorm Y)
BYyr is Element of bool the carrier of (LinearTopSpaceNorm Y)
my0 + BYyr is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ K230((LinearTopSpaceNorm Y),b₁,b₂) where b₁, b₂ is Element of the carrier of (LinearTopSpaceNorm Y) : ( b₁ in my0 & b₂ in BYyr ) } is set
(Cl TBnx01) + (Cl TBnx01) is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ K230((LinearTopSpaceNorm Y),b₁,b₂) where b₁, b₂ is Element of the carrier of (LinearTopSpaceNorm Y) : ( b₁ in Cl TBnx01 & b₂ in Cl TBnx01 ) } is set
(- yy0) + BYyr is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ K230((LinearTopSpaceNorm Y),(- yy0),b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in BYyr } is set
(- y0) + (Ball (y0,r)) is Element of bool the carrier of Y
{ K230(Y,(- y0),b₁) where b₁ is Element of the carrier of Y : b₁ in Ball (y0,r) } is set
TBnx01 + TBnx01 is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ K230((LinearTopSpaceNorm Y),b₁,b₂) where b₁, b₂ is Element of the carrier of (LinearTopSpaceNorm Y) : ( b₁ in TBnx01 & b₂ in TBnx01 ) } is set
Cl (TBnx01 + TBnx01) is closed Element of bool the carrier of (LinearTopSpaceNorm Y)
y0 + (Ball ((0. Y),r)) is Element of bool the carrier of Y
{ K230(Y,y0,b₁) where b₁ is Element of the carrier of Y : b₁ in Ball ((0. Y),r) } is set
BYr is Element of bool the carrier of (LinearTopSpaceNorm Y)
yy0 + BYr is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ K230((LinearTopSpaceNorm Y),yy0,b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in BYr } is set
(- yy0) + yy0 is Element of the carrier of (LinearTopSpaceNorm Y)
the U7 of (LinearTopSpaceNorm Y) is non empty V16() V19([: the carrier of (LinearTopSpaceNorm Y), the carrier of (LinearTopSpaceNorm Y):]) V20( the carrier of (LinearTopSpaceNorm Y)) Function-like V26([: the carrier of (LinearTopSpaceNorm Y), the carrier of (LinearTopSpaceNorm Y):]) quasi_total Element of bool [:[: the carrier of (LinearTopSpaceNorm Y), the carrier of (LinearTopSpaceNorm Y):], the carrier of (LinearTopSpaceNorm Y):]
[: the carrier of (LinearTopSpaceNorm Y), the carrier of (LinearTopSpaceNorm Y):] is non empty set
[:[: the carrier of (LinearTopSpaceNorm Y), the carrier of (LinearTopSpaceNorm Y):], the carrier of (LinearTopSpaceNorm Y):] is non empty set
bool [:[: the carrier of (LinearTopSpaceNorm Y), the carrier of (LinearTopSpaceNorm Y):], the carrier of (LinearTopSpaceNorm Y):] is non empty set
K179( the carrier of (LinearTopSpaceNorm Y), the U7 of (LinearTopSpaceNorm Y),(- yy0),yy0) is Element of the carrier of (LinearTopSpaceNorm Y)
((- yy0) + yy0) + BYr is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ K230((LinearTopSpaceNorm Y),((- yy0) + yy0),b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in BYr } is set
0. (LinearTopSpaceNorm Y) is zero Element of the carrier of (LinearTopSpaceNorm Y)
(0. (LinearTopSpaceNorm Y)) + BYr is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ K230((LinearTopSpaceNorm Y),(0. (LinearTopSpaceNorm Y)),b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in BYr } is set
{(0. (LinearTopSpaceNorm Y))} is Element of bool the carrier of (LinearTopSpaceNorm Y)
{(0. (LinearTopSpaceNorm Y))} + BYr is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ K230((LinearTopSpaceNorm Y),b₁,b₂) where b₁, b₂ is Element of the carrier of (LinearTopSpaceNorm Y) : ( b₁ in {(0. (LinearTopSpaceNorm Y))} & b₂ in BYr ) } is set
1 * TBnx01 is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ (1 * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in TBnx01 } is set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative Element of NAT
(1 + 1) * TBnx01 is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ ((1 + 1) * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in TBnx01 } is set
2 * TBnx01 is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ (2 * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in TBnx01 } is set
(n0 + 1) * 1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
Ball ((0. X),((n0 + 1) * 1)) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not (n0 + 1) * 1 <= ||.((0. X) - b₁).|| } is set
(n0 + 1) * (Ball ((0. X),1)) is Element of bool the carrier of X
{ ((n0 + 1) * b₁) where b₁ is Element of the carrier of X : b₁ in Ball ((0. X),1) } is set
TBX1 is Element of bool the carrier of Y
(n0 + 1) * TBX1 is Element of bool the carrier of Y
{ ((n0 + 1) * b₁) where b₁ is Element of the carrier of Y : b₁ in TBX1 } is set
TB1 is Element of bool the carrier of (LinearTopSpaceNorm Y)
(n0 + 1) * TB1 is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ ((n0 + 1) * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in TB1 } is set
2 * ((n0 + 1) * TB1) is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ (2 * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in (n0 + 1) * TB1 } is set
2 * (n0 + 1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative Element of NAT
(2 * (n0 + 1)) * TB1 is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ ((2 * (n0 + 1)) * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in TB1 } is set
((2 * n0) + 2) * TB1 is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ (((2 * n0) + 2) * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in TB1 } is set
Cl TB1 is closed Element of bool the carrier of (LinearTopSpaceNorm Y)
((2 * n0) + 2) * (Cl TB1) is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ (((2 * n0) + 2) * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in Cl TB1 } is set
r * 1 is complex real ext-real Element of REAL
(r * 1) / ((2 * n0) + 2) is complex real ext-real Element of REAL
Ball ((0. Y),((r * 1) / ((2 * n0) + 2))) is Element of bool the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : not (r * 1) / ((2 * n0) + 2) <= ||.((0. Y) - b₁).|| } is set
r * (1 / ((2 * n0) + 2)) is complex real ext-real Element of REAL
Ball ((0. Y),(r * (1 / ((2 * n0) + 2)))) is Element of bool the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : not r * (1 / ((2 * n0) + 2)) <= ||.((0. Y) - b₁).|| } is set
nb1 is non empty complex real ext-real Element of REAL
nb1 * (Ball ((0. Y),r)) is Element of bool the carrier of Y
{ (nb1 * b₁) where b₁ is Element of the carrier of Y : b₁ in Ball ((0. Y),r) } is set
nb1 * BYr is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ (nb1 * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in BYr } is set
(1 / ((2 * n0) + 2)) * (((2 * n0) + 2) * (Cl TB1)) is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ ((1 / ((2 * n0) + 2)) * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in ((2 * n0) + 2) * (Cl TB1) } is set
(1 / ((2 * n0) + 2)) * ((2 * n0) + 2) is complex real ext-real non negative Element of REAL
((1 / ((2 * n0) + 2)) * ((2 * n0) + 2)) * (Cl TB1) is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ (((1 / ((2 * n0) + 2)) * ((2 * n0) + 2)) * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in Cl TB1 } is set
1 * (Cl TB1) is Element of bool the carrier of (LinearTopSpaceNorm Y)
{ (1 * b₁) where b₁ is Element of the carrier of (LinearTopSpaceNorm Y) : b₁ in Cl TB1 } is set
x is complex real ext-real Element of REAL
Ball ((0. X),x) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not x <= ||.((0. X) - b₁).|| } is set
T .: (Ball ((0. X),x)) is Element of bool the carrier of Y
x * (Ball ((0. X),1)) is Element of bool the carrier of X
{ (x * b₁) where b₁ is Element of the carrier of X : b₁ in Ball ((0. X),1) } is set
x * 1 is complex real ext-real Element of REAL
Ball ((0. X),(x * 1)) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not x * 1 <= ||.((0. X) - b₁).|| } is set
(r / ((2 * n0) + 2)) * x is complex real ext-real Element of REAL
Ball ((0. Y),((r / ((2 * n0) + 2)) * x)) is Element of bool the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : not (r / ((2 * n0) + 2)) * x <= ||.((0. Y) - b₁).|| } is set
x * (Ball ((0. Y),(r / ((2 * n0) + 2)))) is Element of bool the carrier of Y
{ (x * b₁) where b₁ is Element of the carrier of Y : b₁ in Ball ((0. Y),(r / ((2 * n0) + 2))) } is set
y is Element of bool the carrier of Y
x * y is Element of bool the carrier of Y
{ (x * b₁) where b₁ is Element of the carrier of Y : b₁ in y } is set
y is Element of the carrier of Y
x is Element of the carrier of X
T . x is Element of the carrier of Y
p is complex real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of X : not p <= ||.(x - b₁).|| } is set
Ball ((0. X),p) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not p <= ||.((0. X) - b₁).|| } is set
T .: (Ball ((0. X),p)) is Element of bool the carrier of Y
TBp is Element of bool the carrier of Y
q is complex real ext-real Element of REAL
Ball ((0. Y),q) is Element of bool the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : not q <= ||.((0. Y) - b₁).|| } is set
Ball (x,p) is Element of bool the carrier of X
x + (Ball ((0. X),p)) is Element of bool the carrier of X
{ K230(X,x,b₁) where b₁ is Element of the carrier of X : b₁ in Ball ((0. X),p) } is set
q is set
y + TBp is Element of bool the carrier of Y
{ K230(Y,y,b₁) where b₁ is Element of the carrier of Y : b₁ in TBp } is set
t is Element of the carrier of Y
y + t is Element of the carrier of Y
K179( the carrier of Y, the U7 of Y,y,t) is Element of the carrier of Y
z0 is Element of the carrier of X
T . z0 is Element of the carrier of Y
z0 is Element of the carrier of X
x + z0 is Element of the carrier of X
the U7 of X is non empty V16() V19([: the carrier of X, the carrier of X:]) V20( the carrier of X) Function-like V26([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
K179( the carrier of X, the U7 of X,x,z0) is Element of the carrier of X
T . (x + z0) is Element of the carrier of Y
T .: G is Element of bool the carrier of Y
t is set
q is complex real ext-real Element of REAL
Ball ((0. Y),q) is Element of bool the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : not q <= ||.((0. Y) - b₁).|| } is set
y + (Ball ((0. Y),q)) is Element of bool the carrier of Y
{ K230(Y,y,b₁) where b₁ is Element of the carrier of Y : b₁ in Ball ((0. Y),q) } is set
z0 is Element of the carrier of Y
y + z0 is Element of the carrier of Y
K179( the carrier of Y, the U7 of Y,y,z0) is Element of the carrier of Y
Ball (y,q) is Element of bool the carrier of Y
{ b₁ where b₁ is Element of the carrier of Y : not q <= ||.(y - b₁).|| } is set