:: LOPBAN_5 semantic presentation

REAL is non empty V43() V163() V164() V165() V169() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V43() V163() V169() set
omega is non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() set
bool omega is non empty set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
INT is non empty V43() V163() V164() V165() V166() V167() V169() set
[:1,1:] is non empty RAT -valued INT -valued V33() V34() V35() V36() set
RAT is non empty V43() V163() V164() V165() V166() V169() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty RAT -valued INT -valued V33() V34() V35() V36() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty V33() V34() V35() set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is non empty V33() V34() V35() set
[:[:REAL,REAL:],REAL:] is non empty V33() V34() V35() set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
[:2,2:] is non empty RAT -valued INT -valued V33() V34() V35() V36() set
[:[:2,2:],REAL:] is non empty V33() V34() V35() set
bool [:[:2,2:],REAL:] is non empty set
bool NAT is non empty set
[:NAT,REAL:] is non empty V33() V34() V35() set
bool [:NAT,REAL:] is non empty set
ExtREAL is non empty V164() set
bool (bool REAL) is non empty set
K364() is non empty set
[:K364(),K364():] is non empty set
[:[:K364(),K364():],K364():] is non empty set
bool [:[:K364(),K364():],K364():] is non empty set
[:REAL,K364():] is non empty set
[:[:REAL,K364():],K364():] is non empty set
bool [:[:REAL,K364():],K364():] is non empty set
K370() is RLSStruct
the carrier of K370() is set
bool the carrier of K370() is non empty set
K374() is Element of bool the carrier of K370()
[:K374(),K374():] is set
[:[:K374(),K374():],REAL:] is V33() V34() V35() set
bool [:[:K374(),K374():],REAL:] is non empty set
the_set_of_l1RealSequences is Element of bool the carrier of K370()
[:the_set_of_l1RealSequences,REAL:] is V33() V34() V35() set
bool [:the_set_of_l1RealSequences,REAL:] is non empty set
bool [:REAL,REAL:] is non empty set
[:COMPLEX,COMPLEX:] is non empty V33() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is non empty V33() V34() V35() set
bool [:COMPLEX,REAL:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V33() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:RAT,RAT:] is non empty RAT -valued V33() V34() V35() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty RAT -valued V33() V34() V35() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty RAT -valued INT -valued V33() V34() V35() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty RAT -valued INT -valued V33() V34() V35() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty RAT -valued INT -valued V33() V34() V35() V36() set
[:[:NAT,NAT:],NAT:] is non empty RAT -valued INT -valued V33() V34() V35() V36() set
bool [:[:NAT,NAT:],NAT:] is non empty set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V163() V164() V165() V166() V167() V168() V169() set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V163() V164() V165() V166() V167() V168() V169() V207() V230() Element of NAT
- 1 is V11() real ext-real non positive Element of REAL
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
lim_inf X is V11() real ext-real Element of REAL
inferior_realsequence X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
upper_bound (inferior_realsequence X) is V11() real ext-real Element of REAL
K562(REAL,(inferior_realsequence X)) is V163() V164() V165() Element of bool REAL
upper_bound K562(REAL,(inferior_realsequence X)) is V11() real ext-real Element of REAL
Y is V11() real ext-real Element of REAL
Y (#) X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
lim_inf (Y (#) X) is V11() real ext-real Element of REAL
inferior_realsequence (Y (#) X) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
upper_bound (inferior_realsequence (Y (#) X)) is V11() real ext-real Element of REAL
K562(REAL,(inferior_realsequence (Y (#) X))) is V163() V164() V165() Element of bool REAL
upper_bound K562(REAL,(inferior_realsequence (Y (#) X))) is V11() real ext-real Element of REAL
Y * (lim_inf X) is V11() real ext-real Element of REAL
Funcs (NAT,REAL) is non empty functional FUNCTION_DOMAIN of NAT , REAL
(inferior_realsequence X) . 0 is V11() real ext-real Element of REAL
rng (inferior_realsequence X) is V163() V164() V165() set
vseq is Relation-like Function-like set
dom vseq is set
rng vseq is set
tseq is V11() real ext-real set
vseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
X ^\ vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
rng (X ^\ vseq) is V163() V164() V165() set
tseq is Relation-like Function-like set
dom tseq is set
rng tseq is set
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
(X ^\ vseq) . tseq is V11() real ext-real Element of REAL
abs ((X ^\ vseq) . tseq) is V11() real ext-real Element of REAL
vseq + tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
X . (vseq + tseq) is V11() real ext-real Element of REAL
abs (X . (vseq + tseq)) is V11() real ext-real Element of REAL
tseq is non empty V163() V164() V165() Element of bool REAL
(inferior_realsequence (Y (#) X)) . vseq is V11() real ext-real Element of REAL
(Y (#) X) ^\ vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
lower_bound ((Y (#) X) ^\ vseq) is V11() real ext-real Element of REAL
K562(REAL,((Y (#) X) ^\ vseq)) is V163() V164() V165() Element of bool REAL
lower_bound K562(REAL,((Y (#) X) ^\ vseq)) is V11() real ext-real Element of REAL
Y (#) (X ^\ vseq) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
lower_bound (Y (#) (X ^\ vseq)) is V11() real ext-real Element of REAL
K562(REAL,(Y (#) (X ^\ vseq))) is V163() V164() V165() Element of bool REAL
lower_bound K562(REAL,(Y (#) (X ^\ vseq))) is V11() real ext-real Element of REAL
Y ** tseq is V163() V164() V165() Element of bool REAL
lower_bound (Y ** tseq) is V11() real ext-real Element of REAL
lower_bound (X ^\ vseq) is V11() real ext-real Element of REAL
K562(REAL,(X ^\ vseq)) is V163() V164() V165() Element of bool REAL
lower_bound K562(REAL,(X ^\ vseq)) is V11() real ext-real Element of REAL
Y * (lower_bound (X ^\ vseq)) is V11() real ext-real Element of REAL
(inferior_realsequence X) . vseq is V11() real ext-real Element of REAL
Y * ((inferior_realsequence X) . vseq) is V11() real ext-real Element of REAL
Y (#) (inferior_realsequence X) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
(Y (#) (inferior_realsequence X)) . vseq is V11() real ext-real Element of REAL
rng (inferior_realsequence (Y (#) X)) is V163() V164() V165() set
X0 is non empty V163() V164() V165() Element of bool REAL
Y ** X0 is V163() V164() V165() Element of bool REAL
X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
lim_sup X is V11() real ext-real Element of REAL
superior_realsequence X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
lower_bound (superior_realsequence X) is V11() real ext-real Element of REAL
K562(REAL,(superior_realsequence X)) is V163() V164() V165() Element of bool REAL
lower_bound K562(REAL,(superior_realsequence X)) is V11() real ext-real Element of REAL
Y is V11() real ext-real Element of REAL
Y (#) X is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
lim_sup (Y (#) X) is V11() real ext-real Element of REAL
superior_realsequence (Y (#) X) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
lower_bound (superior_realsequence (Y (#) X)) is V11() real ext-real Element of REAL
K562(REAL,(superior_realsequence (Y (#) X))) is V163() V164() V165() Element of bool REAL
lower_bound K562(REAL,(superior_realsequence (Y (#) X))) is V11() real ext-real Element of REAL
Y * (lim_sup X) is V11() real ext-real Element of REAL
Funcs (NAT,REAL) is non empty functional FUNCTION_DOMAIN of NAT , REAL
(superior_realsequence X) . 0 is V11() real ext-real Element of REAL
rng (superior_realsequence X) is V163() V164() V165() set
vseq is Relation-like Function-like set
dom vseq is set
rng vseq is set
tseq is V11() real ext-real set
vseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
X ^\ vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
rng (X ^\ vseq) is V163() V164() V165() set
tseq is Relation-like Function-like set
dom tseq is set
rng tseq is set
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
(X ^\ vseq) . tseq is V11() real ext-real Element of REAL
abs ((X ^\ vseq) . tseq) is V11() real ext-real Element of REAL
vseq + tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
X . (vseq + tseq) is V11() real ext-real Element of REAL
abs (X . (vseq + tseq)) is V11() real ext-real Element of REAL
tseq is non empty V163() V164() V165() Element of bool REAL
(superior_realsequence (Y (#) X)) . vseq is V11() real ext-real Element of REAL
(Y (#) X) ^\ vseq is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
upper_bound ((Y (#) X) ^\ vseq) is V11() real ext-real Element of REAL
K562(REAL,((Y (#) X) ^\ vseq)) is V163() V164() V165() Element of bool REAL
upper_bound K562(REAL,((Y (#) X) ^\ vseq)) is V11() real ext-real Element of REAL
Y (#) (X ^\ vseq) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
upper_bound (Y (#) (X ^\ vseq)) is V11() real ext-real Element of REAL
K562(REAL,(Y (#) (X ^\ vseq))) is V163() V164() V165() Element of bool REAL
upper_bound K562(REAL,(Y (#) (X ^\ vseq))) is V11() real ext-real Element of REAL
Y ** tseq is V163() V164() V165() Element of bool REAL
upper_bound (Y ** tseq) is V11() real ext-real Element of REAL
upper_bound (X ^\ vseq) is V11() real ext-real Element of REAL
K562(REAL,(X ^\ vseq)) is V163() V164() V165() Element of bool REAL
upper_bound K562(REAL,(X ^\ vseq)) is V11() real ext-real Element of REAL
Y * (upper_bound (X ^\ vseq)) is V11() real ext-real Element of REAL
(superior_realsequence X) . vseq is V11() real ext-real Element of REAL
Y * ((superior_realsequence X) . vseq) is V11() real ext-real Element of REAL
Y (#) (superior_realsequence X) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
(Y (#) (superior_realsequence X)) . vseq is V11() real ext-real Element of REAL
rng (superior_realsequence (Y (#) X)) is V163() V164() V165() set
X0 is non empty V163() V164() V165() Element of bool REAL
Y ** X0 is V163() V164() V165() Element of bool REAL
X is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete NORMSTR
MetricSpaceNorm X is non empty Reflexive discerning V94() triangle MetrStruct
the carrier of X is non empty set
distance_by_norm_of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined REAL -valued Function-like V23([: the carrier of X, the carrier of X:]) quasi_total V33() V34() V35() 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 non empty V33() V34() V35() set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is strict MetrStruct
the carrier of (MetricSpaceNorm X) is non empty set
[:NAT, the carrier of (MetricSpaceNorm X):] is non empty set
bool [:NAT, the carrier of (MetricSpaceNorm X):] is non empty set
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
Y is non empty Relation-like NAT -defined the carrier of (MetricSpaceNorm X) -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of (MetricSpaceNorm X):]
X0 is non empty Relation-like NAT -defined the carrier of X -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of X:]
vseq is V11() real ext-real Element of REAL
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
Y . tseq is Element of the carrier of (MetricSpaceNorm X)
Y . tseq is Element of the carrier of (MetricSpaceNorm X)
dist ((Y . tseq),(Y . tseq)) is V11() real ext-real Element of REAL
the distance of (MetricSpaceNorm X) is non empty Relation-like [: the carrier of (MetricSpaceNorm X), the carrier of (MetricSpaceNorm X):] -defined REAL -valued Function-like V23([: the carrier of (MetricSpaceNorm X), the carrier of (MetricSpaceNorm X):]) quasi_total V33() V34() V35() Element of bool [:[: the carrier of (MetricSpaceNorm X), the carrier of (MetricSpaceNorm X):],REAL:]
[: the carrier of (MetricSpaceNorm X), the carrier of (MetricSpaceNorm X):] is non empty set
[:[: the carrier of (MetricSpaceNorm X), the carrier of (MetricSpaceNorm X):],REAL:] is non empty V33() V34() V35() set
bool [:[: the carrier of (MetricSpaceNorm X), the carrier of (MetricSpaceNorm X):],REAL:] is non empty set
the distance of (MetricSpaceNorm X) . ((Y . tseq),(Y . tseq)) is V11() real ext-real Element of REAL
X0 . tseq is Element of the carrier of X
X0 . tseq is Element of the carrier of X
dist ((X0 . tseq),(X0 . tseq)) is V11() real ext-real Element of REAL
(X0 . tseq) - (X0 . tseq) is Element of the carrier of X
- (X0 . tseq) is Element of the carrier of X
K222(X,(X0 . tseq),(- (X0 . tseq))) is Element of the carrier of X
||.((X0 . tseq) - (X0 . tseq)).|| is V11() real ext-real non negative Element of REAL
the U10 of X is non empty Relation-like the carrier of X -defined REAL -valued Function-like V23( the carrier of X) quasi_total V33() V34() V35() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of X,REAL:] is non empty set
the U10 of X . ((X0 . tseq) - (X0 . tseq)) is V11() real ext-real Element of REAL
X is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like NORMSTR
the carrier of X is non empty set
X0 is V11() real ext-real set
Y is Element of the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not X0 <= ||.(Y - b₁).|| } is set
bool the carrier of X is non empty set
{ b₁ where b₁ is Element of the carrier of X : S₁[b₁] } is set
X is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete NORMSTR
the carrier of X is non empty set
K323( the carrier of X) is non empty Element of bool (bool the carrier of X)
bool the carrier of X is non empty set
bool (bool the carrier of X) is non empty set
[:NAT,K323( the carrier of X):] is non empty set
bool [:NAT,K323( the carrier of X):] is non empty set
Y is non empty Relation-like NAT -defined K323( the carrier of X) -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT,K323( the carrier of X):]
rng Y is set
union (rng Y) is set
TopSpaceNorm X is non empty TopSpace-like TopStruct
MetricSpaceNorm X is non empty Reflexive discerning V94() triangle complete MetrStruct
distance_by_norm_of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined REAL -valued Function-like V23([: the carrier of X, the carrier of X:]) quasi_total V33() V34() V35() 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 non empty V33() V34() V35() set
bool [:[: the carrier of X, the carrier of X:],REAL:] is non empty set
MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is strict MetrStruct
TopSpaceMetr (MetricSpaceNorm X) is TopStruct
the carrier of (MetricSpaceNorm X) is non empty set
Family_open_set (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),(Family_open_set (MetricSpaceNorm X)) #) is strict TopStruct
the carrier of (TopSpaceNorm X) is non empty set
bool the carrier of (TopSpaceNorm X) is non empty set
X0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
Y . X0 is Element of K323( the carrier of X)
vseq is Element of bool the carrier of (TopSpaceNorm X)
vseq ` is Element of bool the carrier of (TopSpaceNorm X)
(Y . X0) ` is Element of bool the carrier of X
vseq is V11() real ext-real Element of REAL
tseq is Element of the carrier of (MetricSpaceNorm X)
Ball (tseq,vseq) is Element of bool the carrier of (MetricSpaceNorm X)
X0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
Y . X0 is Element of K323( the carrier of X)
tseq is Element of the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not vseq <= ||.(tseq - b₁).|| } is set
(X,tseq,vseq) is Element of bool the carrier of X
X is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like NORMSTR
the carrier of X is non empty set
Y is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() 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
X0 is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:]
vseq is V11() real ext-real Element of REAL
tseq is Element of the carrier of X
tseq is Element of the carrier of X
X0 /. tseq is Element of the carrier of Y
X0 . tseq is Element of the carrier of Y
X0 /. tseq is Element of the carrier of Y
X0 . tseq is Element of the carrier of Y
(X0 /. tseq) - (X0 /. tseq) is Element of the carrier of Y
- (X0 /. tseq) is Element of the carrier of Y
K222(Y,(X0 /. tseq),(- (X0 /. tseq))) is Element of the carrier of Y
(- 1) * (X0 . tseq) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([: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 non empty set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
K168( the Mult of Y,(- 1),(X0 . tseq)) is set
(X0 . tseq) + ((- 1) * (X0 . tseq)) is Element of the carrier of Y
(- 1) * tseq is Element of the carrier of X
the Mult of X is non empty Relation-like [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like V23([: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 non empty set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K168( the Mult of X,(- 1),tseq) is set
X0 . ((- 1) * tseq) is Element of the carrier of Y
(X0 . tseq) + (X0 . ((- 1) * tseq)) is Element of the carrier of Y
tseq + ((- 1) * tseq) is Element of the carrier of X
X0 . (tseq + ((- 1) * tseq)) is Element of the carrier of Y
- tseq is Element of the carrier of X
tseq + (- tseq) is Element of the carrier of X
X0 . (tseq + (- tseq)) is Element of the carrier of Y
||.((X0 /. tseq) - (X0 /. tseq)).|| is V11() real ext-real non negative Element of REAL
the U10 of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V33() V34() V35() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of Y,REAL:] is non empty set
the U10 of Y . ((X0 /. tseq) - (X0 /. tseq)) is V11() real ext-real Element of REAL
tseq - tseq is Element of the carrier of X
K222(X,tseq,(- tseq)) is Element of the carrier of X
||.(tseq - tseq).|| is V11() real ext-real non negative Element of REAL
the U10 of X is non empty Relation-like the carrier of X -defined REAL -valued Function-like V23( the carrier of X) quasi_total V33() V34() V35() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of X,REAL:] is non empty set
the U10 of X . (tseq - tseq) is V11() real ext-real Element of REAL
vseq * ||.(tseq - tseq).|| is V11() real ext-real Element of REAL
(vseq * ||.(tseq - tseq).||) + ||.(tseq - tseq).|| is V11() real ext-real Element of REAL
vseq + 1 is V11() real ext-real Element of REAL
(vseq + 1) * ||.(tseq - tseq).|| is V11() real ext-real Element of REAL
dom X0 is set
X0 | the carrier of X is Relation-like set
tseq is Element of the carrier of X
X is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete NORMSTR
the carrier of X is non empty set
Y is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like NORMSTR
R_NormSpace_of_BoundedLinearOperators (X,Y) is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like NORMSTR
BoundedLinearOperators (X,Y) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,Y))
R_VectorSpace_of_LinearOperators (X,Y) is non empty V120() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
LinearOperators (X,Y) is non empty functional Element of bool the carrier of K422( the carrier of X,Y)
K422( the carrier of X,Y) is non empty V120() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of Y is non empty set
Funcs ( the carrier of X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of the carrier of X, the carrier of Y
FuncZero ( the carrier of X,Y) is Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total Element of Funcs ( the carrier of X, the carrier of Y)
0. Y is V59(Y) Element of the carrier of Y
K388( the carrier of Y, the carrier of X,(0. Y)) is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of Y:]
[: 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
FuncAdd ( the carrier of X,Y) is non empty Relation-like [:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):] -defined Funcs ( the carrier of X, the carrier of Y) -valued Function-like V23([:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):]) quasi_total Element of bool [:[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):]
[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
[:[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
bool [:[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
FuncExtMult ( the carrier of X,Y) is non empty Relation-like [:REAL,(Funcs ( the carrier of X, the carrier of Y)):] -defined Funcs ( the carrier of X, the carrier of Y) -valued Function-like V23([:REAL,(Funcs ( the carrier of X, the carrier of Y)):]) quasi_total Element of bool [:[:REAL,(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):]
[:REAL,(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
[:[:REAL,(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
bool [:[:REAL,(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
RLSStruct(# (Funcs ( the carrier of X, the carrier of Y)),(FuncZero ( the carrier of X,Y)),(FuncAdd ( the carrier of X,Y)),(FuncExtMult ( the carrier of X,Y)) #) is strict RLSStruct
the carrier of K422( the carrier of X,Y) is non empty set
bool the carrier of K422( the carrier of X,Y) is non empty set
K373(K422( the carrier of X,Y),(LinearOperators (X,Y))) is Element of LinearOperators (X,Y)
K371(K422( the carrier of X,Y),(LinearOperators (X,Y))) is non empty Relation-like [:(LinearOperators (X,Y)),(LinearOperators (X,Y)):] -defined LinearOperators (X,Y) -valued Function-like V23([:(LinearOperators (X,Y)),(LinearOperators (X,Y)):]) quasi_total Element of bool [:[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):],(LinearOperators (X,Y)):]
[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):] is non empty set
[:[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
bool [:[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
K372(K422( the carrier of X,Y),(LinearOperators (X,Y))) is non empty Relation-like [:REAL,(LinearOperators (X,Y)):] -defined LinearOperators (X,Y) -valued Function-like V23([:REAL,(LinearOperators (X,Y)):]) quasi_total Element of bool [:[:REAL,(LinearOperators (X,Y)):],(LinearOperators (X,Y)):]
[:REAL,(LinearOperators (X,Y)):] is non empty set
[:[:REAL,(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
bool [:[:REAL,(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
RLSStruct(# (LinearOperators (X,Y)),K373(K422( the carrier of X,Y),(LinearOperators (X,Y))),K371(K422( the carrier of X,Y),(LinearOperators (X,Y))),K372(K422( the carrier of X,Y),(LinearOperators (X,Y))) #) is V120() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of (R_VectorSpace_of_LinearOperators (X,Y)) is non empty set
bool the carrier of (R_VectorSpace_of_LinearOperators (X,Y)) is non empty set
K373((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))) is Element of BoundedLinearOperators (X,Y)
K371((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))) is non empty Relation-like [:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):] -defined BoundedLinearOperators (X,Y) -valued Function-like V23([:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):]) quasi_total Element of bool [:[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):]
[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):] is non empty set
[:[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
bool [:[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
K372((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))) is non empty Relation-like [:REAL,(BoundedLinearOperators (X,Y)):] -defined BoundedLinearOperators (X,Y) -valued Function-like V23([:REAL,(BoundedLinearOperators (X,Y)):]) quasi_total Element of bool [:[:REAL,(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):]
[:REAL,(BoundedLinearOperators (X,Y)):] is non empty set
[:[:REAL,(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
bool [:[:REAL,(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
BoundedLinearOperatorsNorm (X,Y) is non empty Relation-like BoundedLinearOperators (X,Y) -defined REAL -valued Function-like V23( BoundedLinearOperators (X,Y)) quasi_total V33() V34() V35() Element of bool [:(BoundedLinearOperators (X,Y)),REAL:]
[:(BoundedLinearOperators (X,Y)),REAL:] is non empty V33() V34() V35() set
bool [:(BoundedLinearOperators (X,Y)),REAL:] is non empty set
NORMSTR(# (BoundedLinearOperators (X,Y)),K373((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))),K371((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))),K372((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))),(BoundedLinearOperatorsNorm (X,Y)) #) is strict NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) is non empty set
bool the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) is non empty set
X0 is Element of bool the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
bool the carrier of X is non empty set
{ ||.(b₁ . a₁).|| where b₁ is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:] : b₁ in X0 } is set
vseq is Element of the carrier of X
{ ||.(b₁ . vseq).|| where b₁ is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:] : b₁ in X0 } is set
tseq is set
tseq is set
tseq is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:]
tseq . vseq is Element of the carrier of Y
||.(tseq . vseq).|| is V11() real ext-real non negative Element of REAL
the U10 of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V33() V34() V35() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of Y,REAL:] is non empty set
the U10 of Y . (tseq . vseq) is V11() real ext-real Element of REAL
[: the carrier of X,(bool REAL):] is non empty set
bool [: the carrier of X,(bool REAL):] is non empty set
vseq is non empty Relation-like the carrier of X -defined bool REAL -valued Function-like V23( the carrier of X) quasi_total Element of bool [: the carrier of X,(bool REAL):]
vseq is non empty Relation-like the carrier of X -defined bool REAL -valued Function-like V23( the carrier of X) quasi_total Element of bool [: the carrier of X,(bool REAL):]
{ b₁ where b₁ is Element of the carrier of X : ( vseq . b₁ is bounded_above & upper_bound (vseq . b₁) <= a₁ ) } is set
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
{ b₁ where b₁ is Element of the carrier of X : ( vseq . b₁ is bounded_above & upper_bound (vseq . b₁) <= tseq ) } is set
tseq is set
tseq is set
c₈ is Element of the carrier of X
vseq . c₈ is V163() V164() V165() Element of bool REAL
upper_bound (vseq . c₈) is V11() real ext-real Element of REAL
[:NAT,(bool the carrier of X):] is non empty set
bool [:NAT,(bool the carrier of X):] is non empty set
tseq is non empty Relation-like NAT -defined bool the carrier of X -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT,(bool the carrier of X):]
tseq is non empty Relation-like NAT -defined bool the carrier of X -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT,(bool the carrier of X):]
K323( the carrier of X) is non empty Element of bool (bool the carrier of X)
bool (bool the carrier of X) is non empty set
[:NAT,K323( the carrier of X):] is non empty set
bool [:NAT,K323( the carrier of X):] is non empty set
tseq is non empty Relation-like NAT -defined K323( the carrier of X) -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT,K323( the carrier of X):]
rng tseq is set
union (rng tseq) is set
tseq is set
c₈ is Element of the carrier of X
x is V11() real ext-real set
vseq . c₈ is V163() V164() V165() Element of bool REAL
{ ||.(b₁ . c₈).|| where b₁ is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:] : b₁ in X0 } is set
TK1 is V11() real ext-real set
V is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:]
V . c₈ is Element of the carrier of Y
||.(V . c₈).|| is V11() real ext-real non negative Element of REAL
the U10 of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V33() V34() V35() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of Y,REAL:] is non empty set
the U10 of Y . (V . c₈) is V11() real ext-real Element of REAL
TK1 is ext-real set
V is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:]
V . c₈ is Element of the carrier of Y
||.(V . c₈).|| is V11() real ext-real non negative Element of REAL
the U10 of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V33() V34() V35() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of Y,REAL:] is non empty set
the U10 of Y . (V . c₈) is V11() real ext-real Element of REAL
TK1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
V is set
V is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:]
V . c₈ is Element of the carrier of Y
||.(V . c₈).|| is V11() real ext-real non negative Element of REAL
the U10 of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V33() V34() V35() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of Y,REAL:] is non empty set
the U10 of Y . (V . c₈) is V11() real ext-real Element of REAL
vseq . tseq is set
upper_bound (vseq . c₈) is V11() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of X : ( vseq . b₁ is bounded_above & upper_bound (vseq . b₁) <= TK1 ) } is set
tseq . TK1 is Element of K323( the carrier of X)
Union tseq is set
tseq is Element of the carrier of X
vseq . tseq is V163() V164() V165() Element of bool REAL
c₈ is set
{ ||.(b₁ . tseq).|| where b₁ is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:] : b₁ in X0 } is set
x is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:]
x . tseq is Element of the carrier of Y
||.(x . tseq).|| is V11() real ext-real non negative Element of REAL
the U10 of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V33() V34() V35() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of Y,REAL:] is non empty set
the U10 of Y . (x . tseq) is V11() real ext-real Element of REAL
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
tseq . tseq is Element of K323( the carrier of X)
[:NAT, the carrier of X:] is non empty set
bool [:NAT, the carrier of X:] is non empty set
c₈ is non empty Relation-like NAT -defined the carrier of X -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of X:]
rng c₈ is set
lim c₈ is Element of the carrier of X
vseq . (lim c₈) is V163() V164() V165() Element of bool REAL
{ ||.(b₁ . (lim c₈)).|| where b₁ is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:] : b₁ in X0 } is set
x is V11() real ext-real set
TK1 is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:]
TK1 . (lim c₈) is Element of the carrier of Y
||.(TK1 . (lim c₈)).|| is V11() real ext-real non negative Element of REAL
the U10 of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V33() V34() V35() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of Y,REAL:] is non empty set
the U10 of Y . (TK1 . (lim c₈)) is V11() real ext-real Element of REAL
dom TK1 is set
TK1 /* c₈ is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( 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
||.(TK1 /* c₈).|| is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
V is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
||.(TK1 /* c₈).|| . V is V11() real ext-real Element of REAL
(TK1 /* c₈) . V is Element of the carrier of Y
||.((TK1 /* c₈) . V).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . ((TK1 /* c₈) . V) is V11() real ext-real Element of REAL
c₈ . V is Element of the carrier of X
TK1 /. (c₈ . V) is Element of the carrier of Y
TK1 . (c₈ . V) is Element of the carrier of Y
||.(TK1 /. (c₈ . V)).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . (TK1 /. (c₈ . V)) is V11() real ext-real Element of REAL
dom c₈ is V163() V164() V165() V166() V167() V168() set
{ b₁ where b₁ is Element of the carrier of X : ( vseq . b₁ is bounded_above & upper_bound (vseq . b₁) <= tseq ) } is set
V is Element of the carrier of X
vseq . V is V163() V164() V165() Element of bool REAL
upper_bound (vseq . V) is V11() real ext-real Element of REAL
{ ||.(b₁ . V).|| where b₁ is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:] : b₁ in X0 } is set
||.(TK1 . (c₈ . V)).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . (TK1 . (c₈ . V)) is V11() real ext-real Element of REAL
vseq . (c₈ . V) is V163() V164() V165() Element of bool REAL
upper_bound (vseq . (c₈ . V)) is V11() real ext-real Element of REAL
V is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
||.(TK1 /* c₈).|| . V is V11() real ext-real Element of REAL
TK1 /. (lim c₈) is Element of the carrier of Y
lim (TK1 /* c₈) is Element of the carrier of Y
lim ||.(TK1 /* c₈).|| is V11() real ext-real Element of REAL
||.(TK1 /. (lim c₈)).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . (TK1 /. (lim c₈)) is V11() real ext-real Element of REAL
x is ext-real set
upper_bound (vseq . (lim c₈)) is V11() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of X : ( vseq . b₁ is bounded_above & upper_bound (vseq . b₁) <= tseq ) } is set
tseq is set
TK1 is V11() real ext-real Element of REAL
V is Element of the carrier of X
(X,V,TK1) is Element of bool the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not TK1 <= ||.(V - b₁).|| } is set
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
tseq . x is Element of K323( the carrier of X)
V - V is Element of the carrier of X
- V is Element of the carrier of X
K222(X,V,(- V)) is Element of the carrier of X
||.(V - V).|| is V11() real ext-real non negative Element of REAL
the U10 of X is non empty Relation-like the carrier of X -defined REAL -valued Function-like V23( the carrier of X) quasi_total V33() V34() V35() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of X,REAL:] is non empty set
the U10 of X . (V - V) is V11() real ext-real Element of REAL
0. X is V59(X) Element of the carrier of X
||.(0. X).|| is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V163() V164() V165() V166() V167() V168() V169() Element of REAL
the U10 of X . (0. X) is V11() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of X : ( vseq . b₁ is bounded_above & upper_bound (vseq . b₁) <= x ) } is set
V is Element of the carrier of X
vseq . V is V163() V164() V165() Element of bool REAL
upper_bound (vseq . V) is V11() real ext-real Element of REAL
{ ||.(b₁ . V).|| where b₁ is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:] : b₁ in X0 } is set
c₈ is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:]
c₈ . V is Element of the carrier of Y
||.(c₈ . V).|| is V11() real ext-real non negative Element of REAL
the U10 of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V33() V34() V35() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of Y,REAL:] is non empty set
the U10 of Y . (c₈ . V) is V11() real ext-real Element of REAL
vseq . V is V163() V164() V165() Element of bool REAL
upper_bound (vseq . V) is V11() real ext-real Element of REAL
s is Element of the carrier of X
||.s.|| is V11() real ext-real non negative Element of REAL
the U10 of X . s is V11() real ext-real Element of REAL
2 * ||.s.|| is V11() real ext-real non negative Element of REAL
TK1 / (2 * ||.s.||) is V11() real ext-real Element of REAL
K39((2 * ||.s.||)) is V11() real ext-real non negative set
K37(TK1,K39((2 * ||.s.||))) is V11() real ext-real set
(TK1 / (2 * ||.s.||)) * s is Element of the carrier of X
the Mult of X is non empty Relation-like [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like V23([: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 non empty set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K168( the Mult of X,(TK1 / (2 * ||.s.||)),s) is set
((TK1 / (2 * ||.s.||)) * s) + V is Element of the carrier of X
||.s.|| " is V11() real ext-real non negative Element of REAL
(||.s.|| ") * s is Element of the carrier of X
K168( the Mult of X,(||.s.|| "),s) is set
y is Element of the carrier of X
TK1 / 2 is V11() real ext-real Element of REAL
K39(2) is non empty V11() real ext-real positive non negative set
K37(TK1,K39(2)) is V11() real ext-real set
(TK1 / 2) * y is Element of the carrier of X
K168( the Mult of X,(TK1 / 2),y) is set
||.((TK1 / 2) * y).|| is V11() real ext-real non negative Element of REAL
the U10 of X . ((TK1 / 2) * y) is V11() real ext-real Element of REAL
abs (TK1 / 2) is V11() real ext-real Element of REAL
||.y.|| is V11() real ext-real non negative Element of REAL
the U10 of X . y is V11() real ext-real Element of REAL
(abs (TK1 / 2)) * ||.y.|| is V11() real ext-real Element of REAL
(((TK1 / (2 * ||.s.||)) * s) + V) - V is Element of the carrier of X
K222(X,(((TK1 / (2 * ||.s.||)) * s) + V),(- V)) is Element of the carrier of X
||.((((TK1 / (2 * ||.s.||)) * s) + V) - V).|| is V11() real ext-real non negative Element of REAL
the U10 of X . ((((TK1 / (2 * ||.s.||)) * s) + V) - V) is V11() real ext-real Element of REAL
V + (- V) is Element of the carrier of X
((TK1 / (2 * ||.s.||)) * s) + (V + (- V)) is Element of the carrier of X
||.(((TK1 / (2 * ||.s.||)) * s) + (V + (- V))).|| is V11() real ext-real non negative Element of REAL
the U10 of X . (((TK1 / (2 * ||.s.||)) * s) + (V + (- V))) is V11() real ext-real Element of REAL
((TK1 / (2 * ||.s.||)) * s) + (0. X) is Element of the carrier of X
||.(((TK1 / (2 * ||.s.||)) * s) + (0. X)).|| is V11() real ext-real non negative Element of REAL
the U10 of X . (((TK1 / (2 * ||.s.||)) * s) + (0. X)) is V11() real ext-real Element of REAL
||.((TK1 / (2 * ||.s.||)) * s).|| is V11() real ext-real non negative Element of REAL
the U10 of X . ((TK1 / (2 * ||.s.||)) * s) is V11() real ext-real Element of REAL
(TK1 / 2) / ||.s.|| is V11() real ext-real Element of REAL
K39(||.s.||) is V11() real ext-real non negative set
K37((TK1 / 2),K39(||.s.||)) is V11() real ext-real set
((TK1 / 2) / ||.s.||) * s is Element of the carrier of X
K168( the Mult of X,((TK1 / 2) / ||.s.||),s) is set
||.(((TK1 / 2) / ||.s.||) * s).|| is V11() real ext-real non negative Element of REAL
the U10 of X . (((TK1 / 2) / ||.s.||) * s) is V11() real ext-real Element of REAL
abs (||.s.|| ") is V11() real ext-real Element of REAL
(abs (||.s.|| ")) * ||.s.|| is V11() real ext-real Element of REAL
V - (((TK1 / (2 * ||.s.||)) * s) + V) is Element of the carrier of X
- (((TK1 / (2 * ||.s.||)) * s) + V) is Element of the carrier of X
K222(X,V,(- (((TK1 / (2 * ||.s.||)) * s) + V))) is Element of the carrier of X
||.(V - (((TK1 / (2 * ||.s.||)) * s) + V)).|| is V11() real ext-real non negative Element of REAL
the U10 of X . (V - (((TK1 / (2 * ||.s.||)) * s) + V)) is V11() real ext-real Element of REAL
(upper_bound (vseq . V)) + x is V11() real ext-real Element of REAL
2 * ((upper_bound (vseq . V)) + x) is V11() real ext-real Element of REAL
(2 * ((upper_bound (vseq . V)) + x)) / TK1 is V11() real ext-real Element of REAL
K39(TK1) is V11() real ext-real set
K37((2 * ((upper_bound (vseq . V)) + x)),K39(TK1)) is V11() real ext-real set
y is V11() real ext-real Element of REAL
n0 is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:]
n is Element of the carrier of X
n0 . n is Element of the carrier of Y
||.(n0 . n).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . (n0 . n) is V11() real ext-real Element of REAL
m is Element of the carrier of X
vseq . m is V163() V164() V165() Element of bool REAL
upper_bound (vseq . m) is V11() real ext-real Element of REAL
{ ||.(b₁ . m).|| where b₁ is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:] : b₁ in X0 } is set
vseq . n is V163() V164() V165() Element of bool REAL
upper_bound (vseq . n) is V11() real ext-real Element of REAL
n0 is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:]
n0 . V is Element of the carrier of Y
||.(n0 . V).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . (n0 . V) is V11() real ext-real Element of REAL
m is Element of the carrier of X
n0 . m is Element of the carrier of Y
||.(n0 . m).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . (n0 . m) is V11() real ext-real Element of REAL
||.m.|| is V11() real ext-real non negative Element of REAL
the U10 of X . m is V11() real ext-real Element of REAL
y * ||.m.|| is V11() real ext-real Element of REAL
2 * ||.m.|| is V11() real ext-real non negative Element of REAL
TK1 / (2 * ||.m.||) is V11() real ext-real Element of REAL
K39((2 * ||.m.||)) is V11() real ext-real non negative set
K37(TK1,K39((2 * ||.m.||))) is V11() real ext-real set
(2 * ||.m.||) / TK1 is V11() real ext-real Element of REAL
K37((2 * ||.m.||),K39(TK1)) is V11() real ext-real set
(TK1 / (2 * ||.m.||)) * m is Element of the carrier of X
the Mult of X is non empty Relation-like [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like V23([: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 non empty set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K168( the Mult of X,(TK1 / (2 * ||.m.||)),m) is set
n0 . ((TK1 / (2 * ||.m.||)) * m) is Element of the carrier of Y
(n0 . ((TK1 / (2 * ||.m.||)) * m)) + (n0 . V) is Element of the carrier of Y
||.((n0 . ((TK1 / (2 * ||.m.||)) * m)) + (n0 . V)).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . ((n0 . ((TK1 / (2 * ||.m.||)) * m)) + (n0 . V)) is V11() real ext-real Element of REAL
||.(n0 . ((TK1 / (2 * ||.m.||)) * m)).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . (n0 . ((TK1 / (2 * ||.m.||)) * m)) is V11() real ext-real Element of REAL
- (n0 . V) is Element of the carrier of Y
||.(- (n0 . V)).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . (- (n0 . V)) is V11() real ext-real Element of REAL
||.(n0 . ((TK1 / (2 * ||.m.||)) * m)).|| - ||.(n0 . V).|| is V11() real ext-real Element of REAL
K38(||.(n0 . V).||) is V11() real ext-real non positive set
K36(||.(n0 . ((TK1 / (2 * ||.m.||)) * m)).||,K38(||.(n0 . V).||)) is V11() real ext-real set
(n0 . ((TK1 / (2 * ||.m.||)) * m)) - (- (n0 . V)) is Element of the carrier of Y
- (- (n0 . V)) is Element of the carrier of Y
K222(Y,(n0 . ((TK1 / (2 * ||.m.||)) * m)),(- (- (n0 . V)))) is Element of the carrier of Y
||.((n0 . ((TK1 / (2 * ||.m.||)) * m)) - (- (n0 . V))).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . ((n0 . ((TK1 / (2 * ||.m.||)) * m)) - (- (n0 . V))) is V11() real ext-real Element of REAL
((TK1 / (2 * ||.m.||)) * m) + V is Element of the carrier of X
n0 . (((TK1 / (2 * ||.m.||)) * m) + V) is Element of the carrier of Y
||.(n0 . (((TK1 / (2 * ||.m.||)) * m) + V)).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . (n0 . (((TK1 / (2 * ||.m.||)) * m) + V)) is V11() real ext-real Element of REAL
x1 is Element of the carrier of X
vseq . x1 is V163() V164() V165() Element of bool REAL
upper_bound (vseq . x1) is V11() real ext-real Element of REAL
{ ||.(b₁ . x1).|| where b₁ is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:] : b₁ in X0 } is set
(TK1 / (2 * ||.m.||)) * ||.(n0 . m).|| is V11() real ext-real Element of REAL
((TK1 / (2 * ||.m.||)) * ||.(n0 . m).||) - (upper_bound (vseq . V)) is V11() real ext-real Element of REAL
K38((upper_bound (vseq . V))) is V11() real ext-real set
K36(((TK1 / (2 * ||.m.||)) * ||.(n0 . m).||),K38((upper_bound (vseq . V)))) is V11() real ext-real set
((TK1 / (2 * ||.m.||)) * ||.(n0 . m).||) - ||.(n0 . V).|| is V11() real ext-real Element of REAL
K36(((TK1 / (2 * ||.m.||)) * ||.(n0 . m).||),K38(||.(n0 . V).||)) is V11() real ext-real set
(TK1 / (2 * ||.m.||)) * (n0 . m) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([: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 non empty set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
K168( the Mult of Y,(TK1 / (2 * ||.m.||)),(n0 . m)) is set
||.((TK1 / (2 * ||.m.||)) * (n0 . m)).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . ((TK1 / (2 * ||.m.||)) * (n0 . m)) is V11() real ext-real Element of REAL
abs (TK1 / (2 * ||.m.||)) is V11() real ext-real Element of REAL
(abs (TK1 / (2 * ||.m.||))) * ||.(n0 . m).|| is V11() real ext-real Element of REAL
- (upper_bound (vseq . V)) is V11() real ext-real Element of REAL
((TK1 / (2 * ||.m.||)) * ||.(n0 . m).||) + (- (upper_bound (vseq . V))) is V11() real ext-real Element of REAL
(((TK1 / (2 * ||.m.||)) * ||.(n0 . m).||) + (- (upper_bound (vseq . V)))) + (upper_bound (vseq . V)) is V11() real ext-real Element of REAL
x + (upper_bound (vseq . V)) is V11() real ext-real Element of REAL
((2 * ||.m.||) / TK1) * ((TK1 / (2 * ||.m.||)) * ||.(n0 . m).||) is V11() real ext-real Element of REAL
((2 * ||.m.||) / TK1) * (x + (upper_bound (vseq . V))) is V11() real ext-real Element of REAL
(TK1 / (2 * ||.m.||)) * ((2 * ||.m.||) / TK1) is V11() real ext-real Element of REAL
((TK1 / (2 * ||.m.||)) * ((2 * ||.m.||) / TK1)) * ||.(n0 . m).|| is V11() real ext-real Element of REAL
1 * ||.(n0 . m).|| is V11() real ext-real non negative Element of REAL
n is Element of the carrier of X
n0 . n is Element of the carrier of Y
||.(n0 . n).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . (n0 . n) is V11() real ext-real Element of REAL
||.n.|| is V11() real ext-real non negative Element of REAL
the U10 of X . n is V11() real ext-real Element of REAL
y * ||.n.|| is V11() real ext-real Element of REAL
0 * (0. X) is Element of the carrier of X
the Mult of X is non empty Relation-like [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like V23([: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 non empty set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K168( the Mult of X,0,(0. X)) is set
n0 . (0 * (0. X)) is Element of the carrier of Y
n0 . (0. X) is Element of the carrier of Y
0 * (n0 . (0. X)) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([: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 non empty set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
K168( the Mult of Y,0,(n0 . (0. X))) is set
{ ||.(n0 . b₁).|| where b₁ is Element of the carrier of X : ||.b₁.|| <= 1 } is set
n is V11() real ext-real set
m is Element of the carrier of X
n0 . m is Element of the carrier of Y
||.(n0 . m).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . (n0 . m) is V11() real ext-real Element of REAL
||.m.|| is V11() real ext-real non negative Element of REAL
the U10 of X . m is V11() real ext-real Element of REAL
y * ||.m.|| is V11() real ext-real Element of REAL
n0 is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
||.n0.|| is V11() real ext-real non negative Element of REAL
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) is non empty Relation-like the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) -defined REAL -valued Function-like V23( the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) quasi_total V33() V34() V35() Element of bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:]
[: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty V33() V34() V35() set
bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty set
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) . n0 is V11() real ext-real Element of REAL
n is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:]
PreNorms n is non empty V163() V164() V165() Element of bool REAL
{ ||.(n . b₁).|| where b₁ is Element of the carrier of X : ||.b₁.|| <= 1 } is set
m is V11() real ext-real set
upper_bound (PreNorms n) is V11() real ext-real Element of REAL
n0 is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
||.n0.|| is V11() real ext-real non negative Element of REAL
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) is non empty Relation-like the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) -defined REAL -valued Function-like V23( the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) quasi_total V33() V34() V35() Element of bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:]
[: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty V33() V34() V35() set
bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty set
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) . n0 is V11() real ext-real Element of REAL
vseq is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
||.vseq.|| is V11() real ext-real non negative Element of REAL
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) is non empty Relation-like the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) -defined REAL -valued Function-like V23( the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) quasi_total V33() V34() V35() Element of bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:]
[: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty V33() V34() V35() set
bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty set
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) . vseq is V11() real ext-real Element of REAL
X is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like NORMSTR
Y is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like NORMSTR
R_NormSpace_of_BoundedLinearOperators (X,Y) is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like NORMSTR
BoundedLinearOperators (X,Y) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,Y))
R_VectorSpace_of_LinearOperators (X,Y) is non empty V120() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
LinearOperators (X,Y) is non empty functional Element of bool the carrier of K422( the carrier of X,Y)
the carrier of X is non empty set
K422( the carrier of X,Y) is non empty V120() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of Y is non empty set
Funcs ( the carrier of X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of the carrier of X, the carrier of Y
FuncZero ( the carrier of X,Y) is Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total Element of Funcs ( the carrier of X, the carrier of Y)
0. Y is V59(Y) Element of the carrier of Y
K388( the carrier of Y, the carrier of X,(0. Y)) is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of Y:]
[: 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
FuncAdd ( the carrier of X,Y) is non empty Relation-like [:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):] -defined Funcs ( the carrier of X, the carrier of Y) -valued Function-like V23([:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):]) quasi_total Element of bool [:[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):]
[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
[:[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
bool [:[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
FuncExtMult ( the carrier of X,Y) is non empty Relation-like [:REAL,(Funcs ( the carrier of X, the carrier of Y)):] -defined Funcs ( the carrier of X, the carrier of Y) -valued Function-like V23([:REAL,(Funcs ( the carrier of X, the carrier of Y)):]) quasi_total Element of bool [:[:REAL,(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):]
[:REAL,(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
[:[:REAL,(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
bool [:[:REAL,(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
RLSStruct(# (Funcs ( the carrier of X, the carrier of Y)),(FuncZero ( the carrier of X,Y)),(FuncAdd ( the carrier of X,Y)),(FuncExtMult ( the carrier of X,Y)) #) is strict RLSStruct
the carrier of K422( the carrier of X,Y) is non empty set
bool the carrier of K422( the carrier of X,Y) is non empty set
K373(K422( the carrier of X,Y),(LinearOperators (X,Y))) is Element of LinearOperators (X,Y)
K371(K422( the carrier of X,Y),(LinearOperators (X,Y))) is non empty Relation-like [:(LinearOperators (X,Y)),(LinearOperators (X,Y)):] -defined LinearOperators (X,Y) -valued Function-like V23([:(LinearOperators (X,Y)),(LinearOperators (X,Y)):]) quasi_total Element of bool [:[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):],(LinearOperators (X,Y)):]
[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):] is non empty set
[:[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
bool [:[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
K372(K422( the carrier of X,Y),(LinearOperators (X,Y))) is non empty Relation-like [:REAL,(LinearOperators (X,Y)):] -defined LinearOperators (X,Y) -valued Function-like V23([:REAL,(LinearOperators (X,Y)):]) quasi_total Element of bool [:[:REAL,(LinearOperators (X,Y)):],(LinearOperators (X,Y)):]
[:REAL,(LinearOperators (X,Y)):] is non empty set
[:[:REAL,(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
bool [:[:REAL,(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
RLSStruct(# (LinearOperators (X,Y)),K373(K422( the carrier of X,Y),(LinearOperators (X,Y))),K371(K422( the carrier of X,Y),(LinearOperators (X,Y))),K372(K422( the carrier of X,Y),(LinearOperators (X,Y))) #) is V120() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of (R_VectorSpace_of_LinearOperators (X,Y)) is non empty set
bool the carrier of (R_VectorSpace_of_LinearOperators (X,Y)) is non empty set
K373((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))) is Element of BoundedLinearOperators (X,Y)
K371((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))) is non empty Relation-like [:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):] -defined BoundedLinearOperators (X,Y) -valued Function-like V23([:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):]) quasi_total Element of bool [:[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):]
[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):] is non empty set
[:[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
bool [:[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
K372((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))) is non empty Relation-like [:REAL,(BoundedLinearOperators (X,Y)):] -defined BoundedLinearOperators (X,Y) -valued Function-like V23([:REAL,(BoundedLinearOperators (X,Y)):]) quasi_total Element of bool [:[:REAL,(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):]
[:REAL,(BoundedLinearOperators (X,Y)):] is non empty set
[:[:REAL,(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
bool [:[:REAL,(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
BoundedLinearOperatorsNorm (X,Y) is non empty Relation-like BoundedLinearOperators (X,Y) -defined REAL -valued Function-like V23( BoundedLinearOperators (X,Y)) quasi_total V33() V34() V35() Element of bool [:(BoundedLinearOperators (X,Y)),REAL:]
[:(BoundedLinearOperators (X,Y)),REAL:] is non empty V33() V34() V35() set
bool [:(BoundedLinearOperators (X,Y)),REAL:] is non empty set
NORMSTR(# (BoundedLinearOperators (X,Y)),K373((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))),K371((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))),K372((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))),(BoundedLinearOperatorsNorm (X,Y)) #) is strict NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) is non empty set
[:NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)):] is non empty set
bool [:NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)):] is non empty set
[:NAT, the carrier of Y:] is non empty set
bool [:NAT, the carrier of Y:] is non empty set
X0 is non empty Relation-like NAT -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)):]
vseq is Element of the carrier of X
tseq is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of Y:]
tseq is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of Y:]
tseq is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
tseq . tseq is Element of the carrier of Y
X0 . tseq is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
(X0 . tseq) . vseq is Element of the carrier of Y
tseq . tseq is Element of the carrier of Y
X is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete NORMSTR
the carrier of X is non empty set
Y is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like NORMSTR
R_NormSpace_of_BoundedLinearOperators (X,Y) is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like NORMSTR
BoundedLinearOperators (X,Y) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,Y))
R_VectorSpace_of_LinearOperators (X,Y) is non empty V120() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
LinearOperators (X,Y) is non empty functional Element of bool the carrier of K422( the carrier of X,Y)
K422( the carrier of X,Y) is non empty V120() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of Y is non empty set
Funcs ( the carrier of X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of the carrier of X, the carrier of Y
FuncZero ( the carrier of X,Y) is Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total Element of Funcs ( the carrier of X, the carrier of Y)
0. Y is V59(Y) Element of the carrier of Y
K388( the carrier of Y, the carrier of X,(0. Y)) is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of Y:]
[: 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
FuncAdd ( the carrier of X,Y) is non empty Relation-like [:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):] -defined Funcs ( the carrier of X, the carrier of Y) -valued Function-like V23([:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):]) quasi_total Element of bool [:[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):]
[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
[:[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
bool [:[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
FuncExtMult ( the carrier of X,Y) is non empty Relation-like [:REAL,(Funcs ( the carrier of X, the carrier of Y)):] -defined Funcs ( the carrier of X, the carrier of Y) -valued Function-like V23([:REAL,(Funcs ( the carrier of X, the carrier of Y)):]) quasi_total Element of bool [:[:REAL,(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):]
[:REAL,(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
[:[:REAL,(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
bool [:[:REAL,(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
RLSStruct(# (Funcs ( the carrier of X, the carrier of Y)),(FuncZero ( the carrier of X,Y)),(FuncAdd ( the carrier of X,Y)),(FuncExtMult ( the carrier of X,Y)) #) is strict RLSStruct
the carrier of K422( the carrier of X,Y) is non empty set
bool the carrier of K422( the carrier of X,Y) is non empty set
K373(K422( the carrier of X,Y),(LinearOperators (X,Y))) is Element of LinearOperators (X,Y)
K371(K422( the carrier of X,Y),(LinearOperators (X,Y))) is non empty Relation-like [:(LinearOperators (X,Y)),(LinearOperators (X,Y)):] -defined LinearOperators (X,Y) -valued Function-like V23([:(LinearOperators (X,Y)),(LinearOperators (X,Y)):]) quasi_total Element of bool [:[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):],(LinearOperators (X,Y)):]
[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):] is non empty set
[:[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
bool [:[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
K372(K422( the carrier of X,Y),(LinearOperators (X,Y))) is non empty Relation-like [:REAL,(LinearOperators (X,Y)):] -defined LinearOperators (X,Y) -valued Function-like V23([:REAL,(LinearOperators (X,Y)):]) quasi_total Element of bool [:[:REAL,(LinearOperators (X,Y)):],(LinearOperators (X,Y)):]
[:REAL,(LinearOperators (X,Y)):] is non empty set
[:[:REAL,(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
bool [:[:REAL,(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
RLSStruct(# (LinearOperators (X,Y)),K373(K422( the carrier of X,Y),(LinearOperators (X,Y))),K371(K422( the carrier of X,Y),(LinearOperators (X,Y))),K372(K422( the carrier of X,Y),(LinearOperators (X,Y))) #) is V120() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of (R_VectorSpace_of_LinearOperators (X,Y)) is non empty set
bool the carrier of (R_VectorSpace_of_LinearOperators (X,Y)) is non empty set
K373((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))) is Element of BoundedLinearOperators (X,Y)
K371((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))) is non empty Relation-like [:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):] -defined BoundedLinearOperators (X,Y) -valued Function-like V23([:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):]) quasi_total Element of bool [:[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):]
[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):] is non empty set
[:[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
bool [:[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
K372((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))) is non empty Relation-like [:REAL,(BoundedLinearOperators (X,Y)):] -defined BoundedLinearOperators (X,Y) -valued Function-like V23([:REAL,(BoundedLinearOperators (X,Y)):]) quasi_total Element of bool [:[:REAL,(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):]
[:REAL,(BoundedLinearOperators (X,Y)):] is non empty set
[:[:REAL,(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
bool [:[:REAL,(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
BoundedLinearOperatorsNorm (X,Y) is non empty Relation-like BoundedLinearOperators (X,Y) -defined REAL -valued Function-like V23( BoundedLinearOperators (X,Y)) quasi_total V33() V34() V35() Element of bool [:(BoundedLinearOperators (X,Y)),REAL:]
[:(BoundedLinearOperators (X,Y)),REAL:] is non empty V33() V34() V35() set
bool [:(BoundedLinearOperators (X,Y)),REAL:] is non empty set
NORMSTR(# (BoundedLinearOperators (X,Y)),K373((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))),K371((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))),K372((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))),(BoundedLinearOperatorsNorm (X,Y)) #) is strict NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) is non empty set
[:NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)):] is non empty set
bool [:NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)):] is non empty set
X0 is non empty Relation-like NAT -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)):]
||.X0.|| is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
lim_inf ||.X0.|| is V11() real ext-real Element of REAL
inferior_realsequence ||.X0.|| is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
upper_bound (inferior_realsequence ||.X0.||) is V11() real ext-real Element of REAL
K562(REAL,(inferior_realsequence ||.X0.||)) is V163() V164() V165() Element of bool REAL
upper_bound K562(REAL,(inferior_realsequence ||.X0.||)) is V11() real ext-real Element of REAL
vseq is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of Y:]
rng X0 is set
tseq is Element of the carrier of X
c₈ is Element of the carrier of X
tseq + c₈ is Element of the carrier of X
vseq . (tseq + c₈) is Element of the carrier of Y
vseq . tseq is Element of the carrier of Y
vseq . c₈ is Element of the carrier of Y
(vseq . tseq) + (vseq . c₈) is Element of the carrier of Y
(X,Y,X0,c₈) is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( 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
lim (X,Y,X0,c₈) is Element of the carrier of Y
(X,Y,X0,(tseq + c₈)) is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of Y:]
lim (X,Y,X0,(tseq + c₈)) is Element of the carrier of Y
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
X0 . x is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
(X,Y,X0,(tseq + c₈)) . x is Element of the carrier of Y
(X0 . x) . (tseq + c₈) is Element of the carrier of Y
(X0 . x) . tseq is Element of the carrier of Y
(X0 . x) . c₈ is Element of the carrier of Y
((X0 . x) . tseq) + ((X0 . x) . c₈) is Element of the carrier of Y
(X,Y,X0,c₈) . x is Element of the carrier of Y
(X,Y,X0,tseq) is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of Y:]
(X,Y,X0,tseq) . x is Element of the carrier of Y
((X,Y,X0,tseq) . x) + ((X,Y,X0,c₈) . x) is Element of the carrier of Y
(X,Y,X0,tseq) + (X,Y,X0,c₈) is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of Y:]
lim (X,Y,X0,tseq) is Element of the carrier of Y
tseq is Element of the carrier of X
(X,Y,X0,tseq) is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( 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
||.(X,Y,X0,tseq).|| is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
c₈ is V11() real ext-real set
x is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
x . tseq is Element of the carrier of Y
||.(x . tseq).|| is V11() real ext-real non negative Element of REAL
the U10 of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V33() V34() V35() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of Y,REAL:] is non empty set
the U10 of Y . (x . tseq) is V11() real ext-real Element of REAL
TK1 is set
X0 . TK1 is set
V is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
X0 . V is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
(X0 . V) . tseq is Element of the carrier of Y
(X,Y,X0,tseq) . V is Element of the carrier of Y
||.(X,Y,X0,tseq).|| . V is V11() real ext-real Element of REAL
||.(X,Y,X0,tseq).|| . 0 is V11() real ext-real Element of REAL
(X,Y,X0,tseq) . 0 is Element of the carrier of Y
||.((X,Y,X0,tseq) . 0).|| is V11() real ext-real non negative Element of REAL
the U10 of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V33() V34() V35() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of Y,REAL:] is non empty set
the U10 of Y . ((X,Y,X0,tseq) . 0) is V11() real ext-real Element of REAL
Funcs (NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) is non empty functional FUNCTION_DOMAIN of NAT , the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
tseq is Relation-like Function-like set
dom tseq is set
rng tseq is set
tseq is V11() real ext-real set
1 + tseq is V11() real ext-real Element of REAL
tseq + 0 is V11() real ext-real Element of REAL
c₈ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
||.X0.|| . c₈ is V11() real ext-real Element of REAL
abs (||.X0.|| . c₈) is V11() real ext-real Element of REAL
X0 . c₈ is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
||.(X0 . c₈).|| is V11() real ext-real non negative Element of REAL
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) is non empty Relation-like the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) -defined REAL -valued Function-like V23( the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) quasi_total V33() V34() V35() Element of bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:]
[: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty V33() V34() V35() set
bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty set
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) . (X0 . c₈) is V11() real ext-real Element of REAL
c₈ is Element of the carrier of X
vseq . c₈ is Element of the carrier of Y
||.(vseq . c₈).|| is V11() real ext-real non negative Element of REAL
the U10 of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V33() V34() V35() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of Y,REAL:] is non empty set
the U10 of Y . (vseq . c₈) is V11() real ext-real Element of REAL
||.c₈.|| is V11() real ext-real non negative Element of REAL
the U10 of X is non empty Relation-like the carrier of X -defined REAL -valued Function-like V23( the carrier of X) quasi_total V33() V34() V35() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of X,REAL:] is non empty set
the U10 of X . c₈ is V11() real ext-real Element of REAL
(lim_inf ||.X0.||) * ||.c₈.|| is V11() real ext-real Element of REAL
||.c₈.|| (#) ||.X0.|| is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
(X,Y,X0,c₈) is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( 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
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
(X,Y,X0,c₈) . x is Element of the carrier of Y
||.((X,Y,X0,c₈) . x).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . ((X,Y,X0,c₈) . x) is V11() real ext-real Element of REAL
X0 . x is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
||.(X0 . x).|| is V11() real ext-real non negative Element of REAL
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) is non empty Relation-like the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) -defined REAL -valued Function-like V23( the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) quasi_total V33() V34() V35() Element of bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:]
[: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty V33() V34() V35() set
bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty set
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) . (X0 . x) is V11() real ext-real Element of REAL
||.(X0 . x).|| * ||.c₈.|| is V11() real ext-real non negative Element of REAL
(X0 . x) . c₈ is Element of the carrier of Y
||.(X,Y,X0,c₈).|| is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
||.(X,Y,X0,c₈).|| . x is V11() real ext-real Element of REAL
(||.c₈.|| (#) ||.X0.||) . x is V11() real ext-real Element of REAL
X0 . x is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
||.(X0 . x).|| is V11() real ext-real non negative Element of REAL
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) is non empty Relation-like the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) -defined REAL -valued Function-like V23( the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) quasi_total V33() V34() V35() Element of bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:]
[: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty V33() V34() V35() set
bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty set
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) . (X0 . x) is V11() real ext-real Element of REAL
||.X0.|| . x is V11() real ext-real Element of REAL
(X,Y,X0,c₈) . x is Element of the carrier of Y
||.((X,Y,X0,c₈) . x).|| is V11() real ext-real non negative Element of REAL
the U10 of Y . ((X,Y,X0,c₈) . x) is V11() real ext-real Element of REAL
||.(X0 . x).|| * ||.c₈.|| is V11() real ext-real non negative Element of REAL
lim_inf (||.c₈.|| (#) ||.X0.||) is V11() real ext-real Element of REAL
inferior_realsequence (||.c₈.|| (#) ||.X0.||) is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
upper_bound (inferior_realsequence (||.c₈.|| (#) ||.X0.||)) is V11() real ext-real Element of REAL
K562(REAL,(inferior_realsequence (||.c₈.|| (#) ||.X0.||))) is V163() V164() V165() Element of bool REAL
upper_bound K562(REAL,(inferior_realsequence (||.c₈.|| (#) ||.X0.||))) is V11() real ext-real Element of REAL
lim (X,Y,X0,c₈) is Element of the carrier of Y
lim ||.(X,Y,X0,c₈).|| is V11() real ext-real Element of REAL
lim_inf ||.(X,Y,X0,c₈).|| is V11() real ext-real Element of REAL
inferior_realsequence ||.(X,Y,X0,c₈).|| is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
upper_bound (inferior_realsequence ||.(X,Y,X0,c₈).||) is V11() real ext-real Element of REAL
K562(REAL,(inferior_realsequence ||.(X,Y,X0,c₈).||)) is V163() V164() V165() Element of bool REAL
upper_bound K562(REAL,(inferior_realsequence ||.(X,Y,X0,c₈).||)) is V11() real ext-real Element of REAL
c₈ is V11() real ext-real set
0 - c₈ is V11() real ext-real Element of REAL
K38(c₈) is V11() real ext-real set
K36(0,K38(c₈)) is V11() real ext-real set
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
0 + x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
||.X0.|| . (0 + x) is V11() real ext-real Element of REAL
X0 . x is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
||.(X0 . x).|| is V11() real ext-real non negative Element of REAL
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) is non empty Relation-like the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) -defined REAL -valued Function-like V23( the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) quasi_total V33() V34() V35() Element of bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:]
[: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty V33() V34() V35() set
bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty set
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) . (X0 . x) is V11() real ext-real Element of REAL
||.X0.|| . x is V11() real ext-real Element of REAL
c₈ is Element of the carrier of X
vseq . c₈ is Element of the carrier of Y
x is V11() real ext-real Element of REAL
x * c₈ is Element of the carrier of X
the Mult of X is non empty Relation-like [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like V23([: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 non empty set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K168( the Mult of X,x,c₈) is set
vseq . (x * c₈) is Element of the carrier of Y
x * (vseq . c₈) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like V23([: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 non empty set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
K168( the Mult of Y,x,(vseq . c₈)) is set
(X,Y,X0,c₈) is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( 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
lim (X,Y,X0,c₈) is Element of the carrier of Y
TK1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
X0 . TK1 is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
(X,Y,X0,(x * c₈)) is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of Y:]
(X,Y,X0,(x * c₈)) . TK1 is Element of the carrier of Y
(X0 . TK1) . (x * c₈) is Element of the carrier of Y
(X0 . TK1) . c₈ is Element of the carrier of Y
x * ((X0 . TK1) . c₈) is Element of the carrier of Y
K168( the Mult of Y,x,((X0 . TK1) . c₈)) is set
(X,Y,X0,c₈) . TK1 is Element of the carrier of Y
x * ((X,Y,X0,c₈) . TK1) is Element of the carrier of Y
K168( the Mult of Y,x,((X,Y,X0,c₈) . TK1)) is set
lim (X,Y,X0,(x * c₈)) is Element of the carrier of Y
x * (X,Y,X0,c₈) is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of Y:]
lim (x * (X,Y,X0,c₈)) is Element of the carrier of Y
{ ||.(vseq . b₁).|| where b₁ is Element of the carrier of X : ||.b₁.|| <= 1 } is set
x is V11() real ext-real set
TK1 is Element of the carrier of X
vseq . TK1 is Element of the carrier of Y
||.(vseq . TK1).|| is V11() real ext-real non negative Element of REAL
the U10 of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V33() V34() V35() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of Y,REAL:] is non empty set
the U10 of Y . (vseq . TK1) is V11() real ext-real Element of REAL
||.TK1.|| is V11() real ext-real non negative Element of REAL
the U10 of X is non empty Relation-like the carrier of X -defined REAL -valued Function-like V23( the carrier of X) quasi_total V33() V34() V35() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of X,REAL:] is non empty set
the U10 of X . TK1 is V11() real ext-real Element of REAL
(lim_inf ||.X0.||) * ||.TK1.|| is V11() real ext-real Element of REAL
c₈ is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:]
PreNorms c₈ is non empty V163() V164() V165() Element of bool REAL
{ ||.(c₈ . b₁).|| where b₁ is Element of the carrier of X : ||.b₁.|| <= 1 } is set
upper_bound (PreNorms c₈) is V11() real ext-real Element of REAL
x is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
||.x.|| is V11() real ext-real non negative Element of REAL
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) is non empty Relation-like the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) -defined REAL -valued Function-like V23( the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) quasi_total V33() V34() V35() Element of bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:]
[: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty V33() V34() V35() set
bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty set
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) . x is V11() real ext-real Element of REAL
x is Element of the carrier of X
vseq . x is Element of the carrier of Y
||.(vseq . x).|| is V11() real ext-real non negative Element of REAL
the U10 of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V33() V34() V35() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of Y,REAL:] is non empty set
the U10 of Y . (vseq . x) is V11() real ext-real Element of REAL
||.x.|| is V11() real ext-real non negative Element of REAL
the U10 of X is non empty Relation-like the carrier of X -defined REAL -valued Function-like V23( the carrier of X) quasi_total V33() V34() V35() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of X,REAL:] is non empty set
the U10 of X . x is V11() real ext-real Element of REAL
(lim_inf ||.X0.||) * ||.x.|| is V11() real ext-real Element of REAL
TK1 is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
||.TK1.|| is V11() real ext-real non negative Element of REAL
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) is non empty Relation-like the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) -defined REAL -valued Function-like V23( the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) quasi_total V33() V34() V35() Element of bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:]
[: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty V33() V34() V35() set
bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty set
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) . TK1 is V11() real ext-real Element of REAL
X is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete NORMSTR
LinearTopSpaceNorm X is non empty TopSpace-like T_2 V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V197() V198() V199() L18()
the carrier of (LinearTopSpaceNorm X) is non empty set
bool the carrier of (LinearTopSpaceNorm X) is non empty set
the carrier of X is non empty set
Y is Element of bool the carrier of (LinearTopSpaceNorm X)
X0 is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete NORMSTR
R_NormSpace_of_BoundedLinearOperators (X,X0) is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete NORMSTR
BoundedLinearOperators (X,X0) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,X0))
R_VectorSpace_of_LinearOperators (X,X0) is non empty V120() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
LinearOperators (X,X0) is non empty functional Element of bool the carrier of K422( the carrier of X,X0)
K422( the carrier of X,X0) is non empty V120() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of X0 is non empty set
Funcs ( the carrier of X, the carrier of X0) is non empty functional FUNCTION_DOMAIN of the carrier of X, the carrier of X0
FuncZero ( the carrier of X,X0) is Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V23( the carrier of X) quasi_total Element of Funcs ( the carrier of X, the carrier of X0)
0. X0 is V59(X0) Element of the carrier of X0
K388( the carrier of X0, the carrier of X,(0. X0)) is non empty Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V23( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of X0:]
[: the carrier of X, the carrier of X0:] is non empty set
bool [: the carrier of X, the carrier of X0:] is non empty set
FuncAdd ( the carrier of X,X0) is non empty Relation-like [:(Funcs ( the carrier of X, the carrier of X0)),(Funcs ( the carrier of X, the carrier of X0)):] -defined Funcs ( the carrier of X, the carrier of X0) -valued Function-like V23([:(Funcs ( the carrier of X, the carrier of X0)),(Funcs ( the carrier of X, the carrier of X0)):]) quasi_total Element of bool [:[:(Funcs ( the carrier of X, the carrier of X0)),(Funcs ( the carrier of X, the carrier of X0)):],(Funcs ( the carrier of X, the carrier of X0)):]
[:(Funcs ( the carrier of X, the carrier of X0)),(Funcs ( the carrier of X, the carrier of X0)):] is non empty set
[:[:(Funcs ( the carrier of X, the carrier of X0)),(Funcs ( the carrier of X, the carrier of X0)):],(Funcs ( the carrier of X, the carrier of X0)):] is non empty set
bool [:[:(Funcs ( the carrier of X, the carrier of X0)),(Funcs ( the carrier of X, the carrier of X0)):],(Funcs ( the carrier of X, the carrier of X0)):] is non empty set
FuncExtMult ( the carrier of X,X0) is non empty Relation-like [:REAL,(Funcs ( the carrier of X, the carrier of X0)):] -defined Funcs ( the carrier of X, the carrier of X0) -valued Function-like V23([:REAL,(Funcs ( the carrier of X, the carrier of X0)):]) quasi_total Element of bool [:[:REAL,(Funcs ( the carrier of X, the carrier of X0)):],(Funcs ( the carrier of X, the carrier of X0)):]
[:REAL,(Funcs ( the carrier of X, the carrier of X0)):] is non empty set
[:[:REAL,(Funcs ( the carrier of X, the carrier of X0)):],(Funcs ( the carrier of X, the carrier of X0)):] is non empty set
bool [:[:REAL,(Funcs ( the carrier of X, the carrier of X0)):],(Funcs ( the carrier of X, the carrier of X0)):] is non empty set
RLSStruct(# (Funcs ( the carrier of X, the carrier of X0)),(FuncZero ( the carrier of X,X0)),(FuncAdd ( the carrier of X,X0)),(FuncExtMult ( the carrier of X,X0)) #) is strict RLSStruct
the carrier of K422( the carrier of X,X0) is non empty set
bool the carrier of K422( the carrier of X,X0) is non empty set
K373(K422( the carrier of X,X0),(LinearOperators (X,X0))) is Element of LinearOperators (X,X0)
K371(K422( the carrier of X,X0),(LinearOperators (X,X0))) is non empty Relation-like [:(LinearOperators (X,X0)),(LinearOperators (X,X0)):] -defined LinearOperators (X,X0) -valued Function-like V23([:(LinearOperators (X,X0)),(LinearOperators (X,X0)):]) quasi_total Element of bool [:[:(LinearOperators (X,X0)),(LinearOperators (X,X0)):],(LinearOperators (X,X0)):]
[:(LinearOperators (X,X0)),(LinearOperators (X,X0)):] is non empty set
[:[:(LinearOperators (X,X0)),(LinearOperators (X,X0)):],(LinearOperators (X,X0)):] is non empty set
bool [:[:(LinearOperators (X,X0)),(LinearOperators (X,X0)):],(LinearOperators (X,X0)):] is non empty set
K372(K422( the carrier of X,X0),(LinearOperators (X,X0))) is non empty Relation-like [:REAL,(LinearOperators (X,X0)):] -defined LinearOperators (X,X0) -valued Function-like V23([:REAL,(LinearOperators (X,X0)):]) quasi_total Element of bool [:[:REAL,(LinearOperators (X,X0)):],(LinearOperators (X,X0)):]
[:REAL,(LinearOperators (X,X0)):] is non empty set
[:[:REAL,(LinearOperators (X,X0)):],(LinearOperators (X,X0)):] is non empty set
bool [:[:REAL,(LinearOperators (X,X0)):],(LinearOperators (X,X0)):] is non empty set
RLSStruct(# (LinearOperators (X,X0)),K373(K422( the carrier of X,X0),(LinearOperators (X,X0))),K371(K422( the carrier of X,X0),(LinearOperators (X,X0))),K372(K422( the carrier of X,X0),(LinearOperators (X,X0))) #) is V120() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of (R_VectorSpace_of_LinearOperators (X,X0)) is non empty set
bool the carrier of (R_VectorSpace_of_LinearOperators (X,X0)) is non empty set
K373((R_VectorSpace_of_LinearOperators (X,X0)),(BoundedLinearOperators (X,X0))) is Element of BoundedLinearOperators (X,X0)
K371((R_VectorSpace_of_LinearOperators (X,X0)),(BoundedLinearOperators (X,X0))) is non empty Relation-like [:(BoundedLinearOperators (X,X0)),(BoundedLinearOperators (X,X0)):] -defined BoundedLinearOperators (X,X0) -valued Function-like V23([:(BoundedLinearOperators (X,X0)),(BoundedLinearOperators (X,X0)):]) quasi_total Element of bool [:[:(BoundedLinearOperators (X,X0)),(BoundedLinearOperators (X,X0)):],(BoundedLinearOperators (X,X0)):]
[:(BoundedLinearOperators (X,X0)),(BoundedLinearOperators (X,X0)):] is non empty set
[:[:(BoundedLinearOperators (X,X0)),(BoundedLinearOperators (X,X0)):],(BoundedLinearOperators (X,X0)):] is non empty set
bool [:[:(BoundedLinearOperators (X,X0)),(BoundedLinearOperators (X,X0)):],(BoundedLinearOperators (X,X0)):] is non empty set
K372((R_VectorSpace_of_LinearOperators (X,X0)),(BoundedLinearOperators (X,X0))) is non empty Relation-like [:REAL,(BoundedLinearOperators (X,X0)):] -defined BoundedLinearOperators (X,X0) -valued Function-like V23([:REAL,(BoundedLinearOperators (X,X0)):]) quasi_total Element of bool [:[:REAL,(BoundedLinearOperators (X,X0)):],(BoundedLinearOperators (X,X0)):]
[:REAL,(BoundedLinearOperators (X,X0)):] is non empty set
[:[:REAL,(BoundedLinearOperators (X,X0)):],(BoundedLinearOperators (X,X0)):] is non empty set
bool [:[:REAL,(BoundedLinearOperators (X,X0)):],(BoundedLinearOperators (X,X0)):] is non empty set
BoundedLinearOperatorsNorm (X,X0) is non empty Relation-like BoundedLinearOperators (X,X0) -defined REAL -valued Function-like V23( BoundedLinearOperators (X,X0)) quasi_total V33() V34() V35() Element of bool [:(BoundedLinearOperators (X,X0)),REAL:]
[:(BoundedLinearOperators (X,X0)),REAL:] is non empty V33() V34() V35() set
bool [:(BoundedLinearOperators (X,X0)),REAL:] is non empty set
NORMSTR(# (BoundedLinearOperators (X,X0)),K373((R_VectorSpace_of_LinearOperators (X,X0)),(BoundedLinearOperators (X,X0))),K371((R_VectorSpace_of_LinearOperators (X,X0)),(BoundedLinearOperators (X,X0))),K372((R_VectorSpace_of_LinearOperators (X,X0)),(BoundedLinearOperators (X,X0))),(BoundedLinearOperatorsNorm (X,X0)) #) is strict NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0)) is non empty set
[:NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0)):] is non empty set
bool [:NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0)):] is non empty set
vseq is non empty Relation-like NAT -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0)) -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0)):]
rng vseq is set
Funcs (NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0))) is non empty functional FUNCTION_DOMAIN of NAT , the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0))
bool the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0)) is non empty set
tseq is Relation-like Function-like set
dom tseq is set
rng tseq is set
tseq is Element of bool the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0))
tseq is Element of the carrier of X
(X,X0,vseq,tseq) is non empty Relation-like NAT -defined the carrier of X0 -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of X0:]
[:NAT, the carrier of X0:] is non empty set
bool [:NAT, the carrier of X0:] is non empty set
c₈ is V11() real ext-real set
x is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0))
TK1 is set
vseq . TK1 is set
x . tseq is Element of the carrier of X0
||.(x . tseq).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 is non empty Relation-like the carrier of X0 -defined REAL -valued Function-like V23( the carrier of X0) quasi_total V33() V34() V35() Element of bool [: the carrier of X0,REAL:]
[: the carrier of X0,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of X0,REAL:] is non empty set
the U10 of X0 . (x . tseq) is V11() real ext-real Element of REAL
V is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
(X,X0,vseq,tseq) . V is Element of the carrier of X0
||.((X,X0,vseq,tseq) . V).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 . ((X,X0,vseq,tseq) . V) is V11() real ext-real Element of REAL
x is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0))
x . tseq is Element of the carrier of X0
||.(x . tseq).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 . (x . tseq) is V11() real ext-real Element of REAL
tseq is V11() real ext-real set
1 + tseq is V11() real ext-real Element of REAL
tseq + 0 is V11() real ext-real Element of REAL
x is non empty Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V23( the carrier of X) quasi_total V226(X,X0) V227(X,X0) Lipschitzian Element of bool [: the carrier of X, the carrier of X0:]
TK1 is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0))
||.TK1.|| is V11() real ext-real non negative Element of REAL
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,X0)) is non empty Relation-like the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0)) -defined REAL -valued Function-like V23( the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0))) quasi_total V33() V34() V35() Element of bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0)),REAL:]
[: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0)),REAL:] is non empty V33() V34() V35() set
bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0)),REAL:] is non empty set
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,X0)) . TK1 is V11() real ext-real Element of REAL
V is Element of the carrier of X
x . V is Element of the carrier of X0
V is Element of the carrier of X
x . V is Element of the carrier of X0
(x . V) - (x . V) is Element of the carrier of X0
- (x . V) is Element of the carrier of X0
K222(X0,(x . V),(- (x . V))) is Element of the carrier of X0
||.((x . V) - (x . V)).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 is non empty Relation-like the carrier of X0 -defined REAL -valued Function-like V23( the carrier of X0) quasi_total V33() V34() V35() Element of bool [: the carrier of X0,REAL:]
[: the carrier of X0,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of X0,REAL:] is non empty set
the U10 of X0 . ((x . V) - (x . V)) is V11() real ext-real Element of REAL
V - V is Element of the carrier of X
- V is Element of the carrier of X
K222(X,V,(- V)) is Element of the carrier of X
||.(V - V).|| is V11() real ext-real non negative Element of REAL
the U10 of X is non empty Relation-like the carrier of X -defined REAL -valued Function-like V23( the carrier of X) quasi_total V33() V34() V35() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of X,REAL:] is non empty set
the U10 of X . (V - V) is V11() real ext-real Element of REAL
(1 + tseq) * ||.(V - V).|| is V11() real ext-real Element of REAL
(- 1) * (x . V) is Element of the carrier of X0
the Mult of X0 is non empty Relation-like [:REAL, the carrier of X0:] -defined the carrier of X0 -valued Function-like V23([:REAL, the carrier of X0:]) quasi_total Element of bool [:[:REAL, the carrier of X0:], the carrier of X0:]
[:REAL, the carrier of X0:] is non empty set
[:[:REAL, the carrier of X0:], the carrier of X0:] is non empty set
bool [:[:REAL, the carrier of X0:], the carrier of X0:] is non empty set
K168( the Mult of X0,(- 1),(x . V)) is set
(x . V) + ((- 1) * (x . V)) is Element of the carrier of X0
||.((x . V) + ((- 1) * (x . V))).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 . ((x . V) + ((- 1) * (x . V))) is V11() real ext-real Element of REAL
(- 1) * V is Element of the carrier of X
the Mult of X is non empty Relation-like [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like V23([: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 non empty set
[:[:REAL, the carrier of X:], the carrier of X:] is non empty set
bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set
K168( the Mult of X,(- 1),V) is set
x . ((- 1) * V) is Element of the carrier of X0
(x . V) + (x . ((- 1) * V)) is Element of the carrier of X0
||.((x . V) + (x . ((- 1) * V))).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 . ((x . V) + (x . ((- 1) * V))) is V11() real ext-real Element of REAL
V + ((- 1) * V) is Element of the carrier of X
x . (V + ((- 1) * V)) is Element of the carrier of X0
||.(x . (V + ((- 1) * V))).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 . (x . (V + ((- 1) * V))) is V11() real ext-real Element of REAL
x . (V - V) is Element of the carrier of X0
||.(x . (V - V)).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 . (x . (V - V)) is V11() real ext-real Element of REAL
||.TK1.|| * ||.(V - V).|| is V11() real ext-real non negative Element of REAL
x is Element of the carrier of X
(X,X0,vseq,x) is non empty Relation-like NAT -defined the carrier of X0 -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of X0:]
[:NAT, the carrier of X0:] is non empty set
bool [:NAT, the carrier of X0:] is non empty set
TK1 is V11() real ext-real Element of REAL
TK1 / 3 is V11() real ext-real Element of REAL
K39(3) is non empty V11() real ext-real positive non negative set
K37(TK1,K39(3)) is V11() real ext-real set
3 * (1 + tseq) is V11() real ext-real Element of REAL
TK1 / (3 * (1 + tseq)) is V11() real ext-real Element of REAL
K39((3 * (1 + tseq))) is V11() real ext-real set
K37(TK1,K39((3 * (1 + tseq)))) is V11() real ext-real set
{ b₁ where b₁ is Element of the carrier of X : not TK1 / (3 * (1 + tseq)) <= ||.(x - b₁).|| } is set
V is set
s is Element of the carrier of X
x - s is Element of the carrier of X
- s is Element of the carrier of X
K222(X,x,(- s)) is Element of the carrier of X
||.(x - s).|| is V11() real ext-real non negative Element of REAL
the U10 of X is non empty Relation-like the carrier of X -defined REAL -valued Function-like V23( the carrier of X) quasi_total V33() V34() V35() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of X,REAL:] is non empty set
the U10 of X . (x - s) is V11() real ext-real Element of REAL
x - x is Element of the carrier of X
- x is Element of the carrier of X
K222(X,x,(- x)) is Element of the carrier of X
||.(x - x).|| is V11() real ext-real non negative Element of REAL
the U10 of X is non empty Relation-like the carrier of X -defined REAL -valued Function-like V23( the carrier of X) quasi_total V33() V34() V35() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of X,REAL:] is non empty set
the U10 of X . (x - x) is V11() real ext-real Element of REAL
V is Element of bool the carrier of (LinearTopSpaceNorm X)
s is set
y is Element of the carrier of X
x - y is Element of the carrier of X
- y is Element of the carrier of X
K222(X,x,(- y)) is Element of the carrier of X
||.(x - y).|| is V11() real ext-real non negative Element of REAL
the U10 of X . (x - y) is V11() real ext-real Element of REAL
(X,X0,vseq,y) is non empty Relation-like NAT -defined the carrier of X0 -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of X0:]
n0 is V11() real ext-real Element of REAL
n0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
(X,X0,vseq,x) . n is Element of the carrier of X0
(X,X0,vseq,x) . m is Element of the carrier of X0
((X,X0,vseq,x) . n) - ((X,X0,vseq,x) . m) is Element of the carrier of X0
- ((X,X0,vseq,x) . m) is Element of the carrier of X0
K222(X0,((X,X0,vseq,x) . n),(- ((X,X0,vseq,x) . m))) is Element of the carrier of X0
||.(((X,X0,vseq,x) . n) - ((X,X0,vseq,x) . m)).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 is non empty Relation-like the carrier of X0 -defined REAL -valued Function-like V23( the carrier of X0) quasi_total V33() V34() V35() Element of bool [: the carrier of X0,REAL:]
[: the carrier of X0,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of X0,REAL:] is non empty set
the U10 of X0 . (((X,X0,vseq,x) . n) - ((X,X0,vseq,x) . m)) is V11() real ext-real Element of REAL
vseq . n is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0))
vseq . m is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,X0))
(X,X0,vseq,y) . m is Element of the carrier of X0
((X,X0,vseq,x) . n) - ((X,X0,vseq,y) . m) is Element of the carrier of X0
- ((X,X0,vseq,y) . m) is Element of the carrier of X0
K222(X0,((X,X0,vseq,x) . n),(- ((X,X0,vseq,y) . m))) is Element of the carrier of X0
||.(((X,X0,vseq,x) . n) - ((X,X0,vseq,y) . m)).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 . (((X,X0,vseq,x) . n) - ((X,X0,vseq,y) . m)) is V11() real ext-real Element of REAL
(X,X0,vseq,y) . n is Element of the carrier of X0
((X,X0,vseq,x) . n) - ((X,X0,vseq,y) . n) is Element of the carrier of X0
- ((X,X0,vseq,y) . n) is Element of the carrier of X0
K222(X0,((X,X0,vseq,x) . n),(- ((X,X0,vseq,y) . n))) is Element of the carrier of X0
||.(((X,X0,vseq,x) . n) - ((X,X0,vseq,y) . n)).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 . (((X,X0,vseq,x) . n) - ((X,X0,vseq,y) . n)) is V11() real ext-real Element of REAL
((X,X0,vseq,y) . n) - ((X,X0,vseq,y) . m) is Element of the carrier of X0
K222(X0,((X,X0,vseq,y) . n),(- ((X,X0,vseq,y) . m))) is Element of the carrier of X0
||.(((X,X0,vseq,y) . n) - ((X,X0,vseq,y) . m)).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 . (((X,X0,vseq,y) . n) - ((X,X0,vseq,y) . m)) is V11() real ext-real Element of REAL
||.(((X,X0,vseq,x) . n) - ((X,X0,vseq,y) . n)).|| + ||.(((X,X0,vseq,y) . n) - ((X,X0,vseq,y) . m)).|| is V11() real ext-real non negative Element of REAL
((X,X0,vseq,y) . m) - ((X,X0,vseq,x) . m) is Element of the carrier of X0
K222(X0,((X,X0,vseq,y) . m),(- ((X,X0,vseq,x) . m))) is Element of the carrier of X0
||.(((X,X0,vseq,y) . m) - ((X,X0,vseq,x) . m)).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 . (((X,X0,vseq,y) . m) - ((X,X0,vseq,x) . m)) is V11() real ext-real Element of REAL
||.(((X,X0,vseq,x) . n) - ((X,X0,vseq,y) . m)).|| + ||.(((X,X0,vseq,y) . m) - ((X,X0,vseq,x) . m)).|| is V11() real ext-real non negative Element of REAL
(||.(((X,X0,vseq,x) . n) - ((X,X0,vseq,y) . n)).|| + ||.(((X,X0,vseq,y) . n) - ((X,X0,vseq,y) . m)).||) + ||.(((X,X0,vseq,y) . m) - ((X,X0,vseq,x) . m)).|| is V11() real ext-real non negative Element of REAL
||.(((X,X0,vseq,x) . n) - ((X,X0,vseq,y) . n)).|| + (TK1 / 3) is V11() real ext-real Element of REAL
(||.(((X,X0,vseq,x) . n) - ((X,X0,vseq,y) . n)).|| + (TK1 / 3)) + ||.(((X,X0,vseq,y) . m) - ((X,X0,vseq,x) . m)).|| is V11() real ext-real Element of REAL
((X,X0,vseq,x) . m) - ((X,X0,vseq,y) . m) is Element of the carrier of X0
K222(X0,((X,X0,vseq,x) . m),(- ((X,X0,vseq,y) . m))) is Element of the carrier of X0
||.(((X,X0,vseq,x) . m) - ((X,X0,vseq,y) . m)).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 . (((X,X0,vseq,x) . m) - ((X,X0,vseq,y) . m)) is V11() real ext-real Element of REAL
(vseq . m) . x is Element of the carrier of X0
((vseq . m) . x) - ((X,X0,vseq,y) . m) is Element of the carrier of X0
K222(X0,((vseq . m) . x),(- ((X,X0,vseq,y) . m))) is Element of the carrier of X0
||.(((vseq . m) . x) - ((X,X0,vseq,y) . m)).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 . (((vseq . m) . x) - ((X,X0,vseq,y) . m)) is V11() real ext-real Element of REAL
g is non empty Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V23( the carrier of X) quasi_total V226(X,X0) V227(X,X0) Lipschitzian Element of bool [: the carrier of X, the carrier of X0:]
g . x is Element of the carrier of X0
g . y is Element of the carrier of X0
(g . x) - (g . y) is Element of the carrier of X0
- (g . y) is Element of the carrier of X0
K222(X0,(g . x),(- (g . y))) is Element of the carrier of X0
||.((g . x) - (g . y)).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 . ((g . x) - (g . y)) is V11() real ext-real Element of REAL
(1 + tseq) * ||.(x - y).|| is V11() real ext-real Element of REAL
(1 + tseq) * (TK1 / (3 * (1 + tseq))) is V11() real ext-real Element of REAL
(TK1 / 3) + (TK1 / 3) is V11() real ext-real Element of REAL
((TK1 / 3) + (TK1 / 3)) + (TK1 / 3) is V11() real ext-real Element of REAL
((TK1 / 3) + (TK1 / 3)) + ||.(((X,X0,vseq,y) . m) - ((X,X0,vseq,x) . m)).|| is V11() real ext-real Element of REAL
(vseq . n) . x is Element of the carrier of X0
((vseq . n) . x) - ((X,X0,vseq,y) . n) is Element of the carrier of X0
K222(X0,((vseq . n) . x),(- ((X,X0,vseq,y) . n))) is Element of the carrier of X0
||.(((vseq . n) . x) - ((X,X0,vseq,y) . n)).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 . (((vseq . n) . x) - ((X,X0,vseq,y) . n)) is V11() real ext-real Element of REAL
f is non empty Relation-like the carrier of X -defined the carrier of X0 -valued Function-like V23( the carrier of X) quasi_total V226(X,X0) V227(X,X0) Lipschitzian Element of bool [: the carrier of X, the carrier of X0:]
f . x is Element of the carrier of X0
f . y is Element of the carrier of X0
(f . x) - (f . y) is Element of the carrier of X0
- (f . y) is Element of the carrier of X0
K222(X0,(f . x),(- (f . y))) is Element of the carrier of X0
||.((f . x) - (f . y)).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 . ((f . x) - (f . y)) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() Element of NAT
(X,X0,vseq,x) . n is Element of the carrier of X0
(X,X0,vseq,x) . m is Element of the carrier of X0
((X,X0,vseq,x) . n) - ((X,X0,vseq,x) . m) is Element of the carrier of X0
- ((X,X0,vseq,x) . m) is Element of the carrier of X0
K222(X0,((X,X0,vseq,x) . n),(- ((X,X0,vseq,x) . m))) is Element of the carrier of X0
||.(((X,X0,vseq,x) . n) - ((X,X0,vseq,x) . m)).|| is V11() real ext-real non negative Element of REAL
the U10 of X0 is non empty Relation-like the carrier of X0 -defined REAL -valued Function-like V23( the carrier of X0) quasi_total V33() V34() V35() Element of bool [: the carrier of X0,REAL:]
[: the carrier of X0,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of X0,REAL:] is non empty set
the U10 of X0 . (((X,X0,vseq,x) . n) - ((X,X0,vseq,x) . m)) is V11() real ext-real Element of REAL
X is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete NORMSTR
LinearTopSpaceNorm X is non empty TopSpace-like T_2 V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V197() V198() V199() L18()
the carrier of (LinearTopSpaceNorm X) is non empty set
bool the carrier of (LinearTopSpaceNorm X) is non empty set
Y is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete NORMSTR
R_NormSpace_of_BoundedLinearOperators (X,Y) is non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete NORMSTR
BoundedLinearOperators (X,Y) is non empty Element of bool the carrier of (R_VectorSpace_of_LinearOperators (X,Y))
R_VectorSpace_of_LinearOperators (X,Y) is non empty V120() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
LinearOperators (X,Y) is non empty functional Element of bool the carrier of K422( the carrier of X,Y)
the carrier of X is non empty set
K422( the carrier of X,Y) is non empty V120() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of Y is non empty set
Funcs ( the carrier of X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of the carrier of X, the carrier of Y
FuncZero ( the carrier of X,Y) is Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total Element of Funcs ( the carrier of X, the carrier of Y)
0. Y is V59(Y) Element of the carrier of Y
K388( the carrier of Y, the carrier of X,(0. Y)) is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of Y:]
[: 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
FuncAdd ( the carrier of X,Y) is non empty Relation-like [:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):] -defined Funcs ( the carrier of X, the carrier of Y) -valued Function-like V23([:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):]) quasi_total Element of bool [:[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):]
[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
[:[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
bool [:[:(Funcs ( the carrier of X, the carrier of Y)),(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
FuncExtMult ( the carrier of X,Y) is non empty Relation-like [:REAL,(Funcs ( the carrier of X, the carrier of Y)):] -defined Funcs ( the carrier of X, the carrier of Y) -valued Function-like V23([:REAL,(Funcs ( the carrier of X, the carrier of Y)):]) quasi_total Element of bool [:[:REAL,(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):]
[:REAL,(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
[:[:REAL,(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
bool [:[:REAL,(Funcs ( the carrier of X, the carrier of Y)):],(Funcs ( the carrier of X, the carrier of Y)):] is non empty set
RLSStruct(# (Funcs ( the carrier of X, the carrier of Y)),(FuncZero ( the carrier of X,Y)),(FuncAdd ( the carrier of X,Y)),(FuncExtMult ( the carrier of X,Y)) #) is strict RLSStruct
the carrier of K422( the carrier of X,Y) is non empty set
bool the carrier of K422( the carrier of X,Y) is non empty set
K373(K422( the carrier of X,Y),(LinearOperators (X,Y))) is Element of LinearOperators (X,Y)
K371(K422( the carrier of X,Y),(LinearOperators (X,Y))) is non empty Relation-like [:(LinearOperators (X,Y)),(LinearOperators (X,Y)):] -defined LinearOperators (X,Y) -valued Function-like V23([:(LinearOperators (X,Y)),(LinearOperators (X,Y)):]) quasi_total Element of bool [:[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):],(LinearOperators (X,Y)):]
[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):] is non empty set
[:[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
bool [:[:(LinearOperators (X,Y)),(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
K372(K422( the carrier of X,Y),(LinearOperators (X,Y))) is non empty Relation-like [:REAL,(LinearOperators (X,Y)):] -defined LinearOperators (X,Y) -valued Function-like V23([:REAL,(LinearOperators (X,Y)):]) quasi_total Element of bool [:[:REAL,(LinearOperators (X,Y)):],(LinearOperators (X,Y)):]
[:REAL,(LinearOperators (X,Y)):] is non empty set
[:[:REAL,(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
bool [:[:REAL,(LinearOperators (X,Y)):],(LinearOperators (X,Y)):] is non empty set
RLSStruct(# (LinearOperators (X,Y)),K373(K422( the carrier of X,Y),(LinearOperators (X,Y))),K371(K422( the carrier of X,Y),(LinearOperators (X,Y))),K372(K422( the carrier of X,Y),(LinearOperators (X,Y))) #) is V120() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of (R_VectorSpace_of_LinearOperators (X,Y)) is non empty set
bool the carrier of (R_VectorSpace_of_LinearOperators (X,Y)) is non empty set
K373((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))) is Element of BoundedLinearOperators (X,Y)
K371((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))) is non empty Relation-like [:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):] -defined BoundedLinearOperators (X,Y) -valued Function-like V23([:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):]) quasi_total Element of bool [:[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):]
[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):] is non empty set
[:[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
bool [:[:(BoundedLinearOperators (X,Y)),(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
K372((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))) is non empty Relation-like [:REAL,(BoundedLinearOperators (X,Y)):] -defined BoundedLinearOperators (X,Y) -valued Function-like V23([:REAL,(BoundedLinearOperators (X,Y)):]) quasi_total Element of bool [:[:REAL,(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):]
[:REAL,(BoundedLinearOperators (X,Y)):] is non empty set
[:[:REAL,(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
bool [:[:REAL,(BoundedLinearOperators (X,Y)):],(BoundedLinearOperators (X,Y)):] is non empty set
BoundedLinearOperatorsNorm (X,Y) is non empty Relation-like BoundedLinearOperators (X,Y) -defined REAL -valued Function-like V23( BoundedLinearOperators (X,Y)) quasi_total V33() V34() V35() Element of bool [:(BoundedLinearOperators (X,Y)),REAL:]
[:(BoundedLinearOperators (X,Y)),REAL:] is non empty V33() V34() V35() set
bool [:(BoundedLinearOperators (X,Y)),REAL:] is non empty set
NORMSTR(# (BoundedLinearOperators (X,Y)),K373((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))),K371((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))),K372((R_VectorSpace_of_LinearOperators (X,Y)),(BoundedLinearOperators (X,Y))),(BoundedLinearOperatorsNorm (X,Y)) #) is strict NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) is non empty set
[:NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)):] is non empty set
bool [:NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)):] is non empty set
X0 is Element of bool the carrier of (LinearTopSpaceNorm X)
vseq is non empty Relation-like NAT -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)):]
||.vseq.|| is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
lim_inf ||.vseq.|| is V11() real ext-real Element of REAL
inferior_realsequence ||.vseq.|| is non empty Relation-like NAT -defined REAL -valued Function-like V23( NAT ) quasi_total V33() V34() V35() Element of bool [:NAT,REAL:]
upper_bound (inferior_realsequence ||.vseq.||) is V11() real ext-real Element of REAL
K562(REAL,(inferior_realsequence ||.vseq.||)) is V163() V164() V165() Element of bool REAL
upper_bound K562(REAL,(inferior_realsequence ||.vseq.||)) is V11() real ext-real Element of REAL
tseq is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total Element of bool [: the carrier of X, the carrier of Y:]
tseq is Element of the carrier of X
(X,Y,vseq,tseq) is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( 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
tseq is non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like V23( the carrier of X) quasi_total V226(X,Y) V227(X,Y) Lipschitzian Element of bool [: the carrier of X, the carrier of Y:]
tseq is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))
||.tseq.|| is V11() real ext-real non negative Element of REAL
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) is non empty Relation-like the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)) -defined REAL -valued Function-like V23( the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))) quasi_total V33() V34() V35() Element of bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:]
[: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty V33() V34() V35() set
bool [: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y)),REAL:] is non empty set
the U10 of (R_NormSpace_of_BoundedLinearOperators (X,Y)) . tseq is V11() real ext-real Element of REAL
c₈ is Element of the carrier of X
(X,Y,vseq,c₈) is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( 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
x is Element of the carrier of X
tseq . x is Element of the carrier of Y
(X,Y,vseq,x) is non empty Relation-like NAT -defined the carrier of Y -valued Function-like V23( NAT ) quasi_total Element of bool [:NAT, the carrier of Y:]
lim (X,Y,vseq,x) is Element of the carrier of Y
TK1 is Element of the carrier of X
tseq . TK1 is Element of the carrier of Y
||.(tseq . TK1).|| is V11() real ext-real non negative Element of REAL
the U10 of Y is non empty Relation-like the carrier of Y -defined REAL -valued Function-like V23( the carrier of Y) quasi_total V33() V34() V35() Element of bool [: the carrier of Y,REAL:]
[: the carrier of Y,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of Y,REAL:] is non empty set
the U10 of Y . (tseq . TK1) is V11() real ext-real Element of REAL
||.TK1.|| is V11() real ext-real non negative Element of REAL
the U10 of X is non empty Relation-like the carrier of X -defined REAL -valued Function-like V23( the carrier of X) quasi_total V33() V34() V35() Element of bool [: the carrier of X,REAL:]
[: the carrier of X,REAL:] is non empty V33() V34() V35() set
bool [: the carrier of X,REAL:] is non empty set
the U10 of X . TK1 is V11() real ext-real Element of REAL
(lim_inf ||.vseq.||) * ||.TK1.|| is V11() real ext-real Element of REAL