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

bool the carrier of X is non empty set

{ b

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

(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

vseq is Element of the carrier of X

{ ||.(b

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

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

tseq is set

tseq is set

c

vseq . c

upper_bound (vseq . c

[: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

x is V11() real ext-real set

vseq . c

{ ||.(b

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

||.(V . c

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

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

||.(V . c

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

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

||.(V . c

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

vseq . tseq is set

upper_bound (vseq . c

{ b

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

{ ||.(b

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

rng c

lim c

vseq . (lim c

{ ||.(b

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

||.(TK1 . (lim c

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

dom TK1 is set

TK1 /* c

[:NAT, the carrier of Y:] is non empty set

bool [:NAT, the carrier of Y:] is non empty set

||.(TK1 /* c

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

(TK1 /* c

||.((TK1 /* c

the U10 of Y . ((TK1 /* c

c

TK1 /. (c

TK1 . (c

||.(TK1 /. (c

the U10 of Y . (TK1 /. (c

dom c

{ b

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

||.(TK1 . (c

the U10 of Y . (TK1 . (c

vseq . (c

upper_bound (vseq . (c

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

TK1 /. (lim c

lim (TK1 /* c

lim ||.(TK1 /* c

||.(TK1 /. (lim c

the U10 of Y . (TK1 /. (lim c

x is ext-real set

upper_bound (vseq . (lim c

{ b

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

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

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

c

c

||.(c

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

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

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

(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

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

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