:: NFCONT_1 semantic presentation

REAL is non empty V54() set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V54() set
RAT is non empty V54() set
INT is non empty V54() set
omega is non empty epsilon-transitive epsilon-connected ordinal set
K6(omega) is set
K6(NAT) is set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is set
K7(COMPLEX,REAL) is set
K6(K7(COMPLEX,REAL)) is set
K7(NAT,REAL) is set
K6(K7(NAT,REAL)) is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non negative set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non negative Element of NAT
- 1 is V11() real ext-real non positive Element of REAL
X is non empty addLoopStr
the carrier of X is non empty set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
S is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
f is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
S - f is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
- f is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
S + (- f) is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
x0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(S - f) . x0 is Element of the carrier of X
(S + (- f)) . x0 is Element of the carrier of X
S . x0 is Element of the carrier of X
f . x0 is Element of the carrier of X
(S . x0) - (f . x0) is Element of the carrier of X
- (f . x0) is Element of the carrier of X
(S . x0) + (- (f . x0)) is Element of the carrier of X
(- f) . x0 is Element of the carrier of X
(S . x0) + ((- f) . x0) is Element of the carrier of X
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
S is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
- S is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
(- 1) * S is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
((- 1) * S) . f is Element of the carrier of X
S . f is Element of the carrier of X
(- 1) * (S . f) is Element of the carrier of X
- (S . f) is Element of the carrier of X
(- S) . f is Element of the carrier of X
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K6( the carrier of X) is set
S is Element of the carrier of X
{ b₁ where b₁ is Element of the carrier of X : not 1 <= ||.(b₁ - S).|| } is set
x0 is set
p is Element of the carrier of X
p - S is Element of the carrier of X
- S is Element of the carrier of X
p + (- S) is Element of the carrier of X
||.(p - S).|| is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is Element of the carrier of X
f is V11() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of X : not f <= ||.(b₁ - S).|| } is set
p is set
x1 is Element of the carrier of X
x1 - S is Element of the carrier of X
- S is Element of the carrier of X
x1 + (- S) is Element of the carrier of X
||.(x1 - S).|| is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is Element of the carrier of X
f is (X,S)
x0 is V11() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of X : not x0 <= ||.(b₁ - S).|| } is set
S - S is Element of the carrier of X
- S is Element of the carrier of X
S + (- S) is Element of the carrier of X
||.(S - S).|| is V11() real ext-real Element of REAL
0. X is V91(X) Element of the carrier of X
||.(0. X).|| is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K6( the carrier of X) is set
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K6( the carrier of X) is set
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K6( the carrier of X) is set
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of X, the carrier of S) is set
K6(K7( the carrier of X, the carrier of S)) is set
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K7( the carrier of X,REAL) is set
K6(K7( the carrier of X,REAL)) is set
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
f is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K7( the carrier of S, the carrier of f) is set
K6(K7( the carrier of S, the carrier of f)) is set
x0 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
rng x0 is Element of K6( the carrier of S)
K6( the carrier of S) is set
x0 . X is Element of the carrier of S
dom x0 is Element of K6(NAT)
p is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
dom p is Element of K6( the carrier of S)
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
S is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
rng S is Element of K6( the carrier of X)
K6( the carrier of X) is set
f is set
dom S is Element of K6(NAT)
x0 is set
S . x0 is set
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
S . p is Element of the carrier of X
x0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
S . x0 is Element of the carrier of X
dom S is Element of K6(NAT)
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
x0 is Element of the carrier of S
f /. x0 is Element of the carrier of X
p is V11() real ext-real Element of REAL
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL
1 / (x1 + 1) is V11() real ext-real non negative Element of REAL
(x1 + 1) " is V11() real ext-real positive non negative Element of REAL
x2 is Element of the carrier of S
x2 - x0 is Element of the carrier of S
- x0 is Element of the carrier of S
x2 + (- x0) is Element of the carrier of S
||.(x2 - x0).|| is V11() real ext-real Element of REAL
f /. x2 is Element of the carrier of X
(f /. x2) - (f /. x0) is Element of the carrier of X
- (f /. x0) is Element of the carrier of X
(f /. x2) + (- (f /. x0)) is Element of the carrier of X
||.((f /. x2) - (f /. x0)).|| is V11() real ext-real Element of REAL
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
x1 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
x2 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
rng x2 is Element of K6( the carrier of S)
dom x2 is Element of K6(NAT)
s9 is set
x1 is set
x2 . x1 is set
s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x2 . s9 is Element of the carrier of S
f /. (x2 . s9) is Element of the carrier of X
(f /. (x2 . s9)) - (f /. x0) is Element of the carrier of X
- (f /. x0) is Element of the carrier of X
(f /. (x2 . s9)) + (- (f /. x0)) is Element of the carrier of X
||.((f /. (x2 . s9)) - (f /. x0)).|| is V11() real ext-real Element of REAL
f /* x2 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
(f /* x2) . s9 is Element of the carrier of X
((f /* x2) . s9) - (f /. x0) is Element of the carrier of X
((f /* x2) . s9) + (- (f /. x0)) is Element of the carrier of X
||.(((f /* x2) . s9) - (f /. x0)).|| is V11() real ext-real Element of REAL
s9 is V11() real ext-real Element of REAL
s9 " is V11() real ext-real Element of REAL
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL
(s9 ") + 0 is V11() real ext-real Element of REAL
1 / (s9 ") is V11() real ext-real Element of REAL
1 / (x1 + 1) is V11() real ext-real non negative Element of REAL
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL
x2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL
1 / (x2 + 1) is V11() real ext-real non negative Element of REAL
1 / (x1 + 1) is V11() real ext-real non negative Element of REAL
x2 . x2 is Element of the carrier of S
(x2 . x2) - x0 is Element of the carrier of S
- x0 is Element of the carrier of S
(x2 . x2) + (- x0) is Element of the carrier of S
||.((x2 . x2) - x0).|| is V11() real ext-real Element of REAL
lim x2 is Element of the carrier of S
lim (f /* x2) is Element of the carrier of X
s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(f /* x2) . s9 is Element of the carrier of X
((f /* x2) . s9) - (f /. x0) is Element of the carrier of X
((f /* x2) . s9) + (- (f /. x0)) is Element of the carrier of X
||.(((f /* x2) . s9) - (f /. x0)).|| is V11() real ext-real Element of REAL
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
rng p is Element of K6( the carrier of S)
lim p is Element of the carrier of S
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
p . x1 is Element of the carrier of S
(p . x1) - x0 is Element of the carrier of S
- x0 is Element of the carrier of S
(p . x1) + (- x0) is Element of the carrier of S
||.((p . x1) - x0).|| is V11() real ext-real Element of REAL
dom p is Element of K6(NAT)
f /. (p . x1) is Element of the carrier of X
(f /. (p . x1)) - (f /. x0) is Element of the carrier of X
- (f /. x0) is Element of the carrier of X
(f /. (p . x1)) + (- (f /. x0)) is Element of the carrier of X
||.((f /. (p . x1)) - (f /. x0)).|| is V11() real ext-real Element of REAL
f /* p is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
(f /* p) . x1 is Element of the carrier of X
((f /* p) . x1) - (f /. x0) is Element of the carrier of X
((f /* p) . x1) + (- (f /. x0)) is Element of the carrier of X
||.(((f /* p) . x1) - (f /. x0)).|| is V11() real ext-real Element of REAL
lim (f /* p) is Element of the carrier of X
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K7( the carrier of X,REAL) is set
K6(K7( the carrier of X,REAL)) is set
S is Element of the carrier of X
f is Relation-like the carrier of X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of X,REAL))
dom f is Element of K6( the carrier of X)
K6( the carrier of X) is set
f /. S is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL
1 / (p + 1) is V11() real ext-real non negative Element of REAL
(p + 1) " is V11() real ext-real positive non negative Element of REAL
x1 is Element of the carrier of X
x1 - S is Element of the carrier of X
- S is Element of the carrier of X
x1 + (- S) is Element of the carrier of X
||.(x1 - S).|| is V11() real ext-real Element of REAL
f /. x1 is V11() real ext-real Element of REAL
(f /. x1) - (f /. S) is V11() real ext-real Element of REAL
abs ((f /. x1) - (f /. S)) is V11() real ext-real Element of REAL
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
p is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
rng x1 is Element of K6( the carrier of X)
dom x1 is Element of K6(NAT)
x2 is set
s9 is set
x1 . s9 is set
x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x1 . x2 is Element of the carrier of X
f /. (x1 . x2) is V11() real ext-real Element of REAL
(f /. (x1 . x2)) - (f /. S) is V11() real ext-real Element of REAL
abs ((f /. (x1 . x2)) - (f /. S)) is V11() real ext-real Element of REAL
f /* x1 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* x1) . x2 is V11() real ext-real Element of REAL
((f /* x1) . x2) - (f /. S) is V11() real ext-real Element of REAL
abs (((f /* x1) . x2) - (f /. S)) is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
x2 " is V11() real ext-real Element of REAL
s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
s9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL
(x2 ") + 0 is V11() real ext-real Element of REAL
1 / (x2 ") is V11() real ext-real Element of REAL
1 / (s9 + 1) is V11() real ext-real non negative Element of REAL
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL
x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of REAL
1 / (x1 + 1) is V11() real ext-real non negative Element of REAL
1 / (x1 + 1) is V11() real ext-real non negative Element of REAL
x1 . x1 is Element of the carrier of X
(x1 . x1) - S is Element of the carrier of X
- S is Element of the carrier of X
(x1 . x1) + (- S) is Element of the carrier of X
||.((x1 . x1) - S).|| is V11() real ext-real Element of REAL
lim x1 is Element of the carrier of X
lim (f /* x1) is V11() real ext-real Element of REAL
x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(f /* x1) . x2 is V11() real ext-real Element of REAL
((f /* x1) . x2) - (f /. S) is V11() real ext-real Element of REAL
abs (((f /* x1) . x2) - (f /. S)) is V11() real ext-real Element of REAL
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
x0 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
rng x0 is Element of K6( the carrier of X)
lim x0 is Element of the carrier of X
p is V11() real ext-real set
x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x0 . x1 is Element of the carrier of X
(x0 . x1) - S is Element of the carrier of X
- S is Element of the carrier of X
(x0 . x1) + (- S) is Element of the carrier of X
||.((x0 . x1) - S).|| is V11() real ext-real Element of REAL
dom x0 is Element of K6(NAT)
f /. (x0 . x1) is V11() real ext-real Element of REAL
(f /. (x0 . x1)) - (f /. S) is V11() real ext-real Element of REAL
abs ((f /. (x0 . x1)) - (f /. S)) is V11() real ext-real Element of REAL
f /* x0 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f /* x0) . x1 is V11() real ext-real Element of REAL
((f /* x0) . x1) - (f /. S) is V11() real ext-real Element of REAL
abs (((f /* x0) . x1) - (f /. S)) is V11() real ext-real Element of REAL
lim (f /* x0) is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
x0 is Element of the carrier of S
f /. x0 is Element of the carrier of X
p is (X,f /. x0)
x1 is V11() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of X : not x1 <= ||.(b₁ - (f /. x0)).|| } is set
x2 is V11() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of S : not x2 <= ||.(b₁ - x0).|| } is set
s9 is (S,x0)
x1 is Element of the carrier of S
f /. x1 is Element of the carrier of X
(f /. x1) - (f /. x0) is Element of the carrier of X
- (f /. x0) is Element of the carrier of X
(f /. x1) + (- (f /. x0)) is Element of the carrier of X
||.((f /. x1) - (f /. x0)).|| is V11() real ext-real Element of REAL
x1 is Element of the carrier of S
x1 - x0 is Element of the carrier of S
- x0 is Element of the carrier of S
x1 + (- x0) is Element of the carrier of S
||.(x1 - x0).|| is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of X : not p <= ||.(b₁ - (f /. x0)).|| } is set
x1 is (X,f /. x0)
x2 is (S,x0)
s9 is V11() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of S : not s9 <= ||.(b₁ - x0).|| } is set
x1 is V11() real ext-real Element of REAL
x1 is Element of the carrier of S
x1 - x0 is Element of the carrier of S
- x0 is Element of the carrier of S
x1 + (- x0) is Element of the carrier of S
||.(x1 - x0).|| is V11() real ext-real Element of REAL
f /. x1 is Element of the carrier of X
(f /. x1) - (f /. x0) is Element of the carrier of X
- (f /. x0) is Element of the carrier of X
(f /. x1) + (- (f /. x0)) is Element of the carrier of X
||.((f /. x1) - (f /. x0)).|| is V11() real ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of S : not x1 <= ||.(b₁ - x0).|| } is set
x2 is Element of the carrier of X
x2 - (f /. x0) is Element of the carrier of X
x2 + (- (f /. x0)) is Element of the carrier of X
||.(x2 - (f /. x0)).|| is V11() real ext-real Element of REAL
x1 is Element of the carrier of S
x1 - x0 is Element of the carrier of S
- x0 is Element of the carrier of S
x1 + (- x0) is Element of the carrier of S
||.(x1 - x0).|| is V11() real ext-real Element of REAL
f /. x1 is Element of the carrier of X
(f /. x1) - (f /. x0) is Element of the carrier of X
- (f /. x0) is Element of the carrier of X
(f /. x1) + (- (f /. x0)) is Element of the carrier of X
||.((f /. x1) - (f /. x0)).|| is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
x0 is Element of the carrier of S
f /. x0 is Element of the carrier of X
p is (X,f /. x0)
x1 is (S,x0)
f .: x1 is Element of K6( the carrier of X)
K6( the carrier of X) is set
x2 is set
s9 is Element of the carrier of S
f . s9 is set
f /. s9 is Element of the carrier of X
p is (X,f /. x0)
x1 is (S,x0)
f .: x1 is Element of K6( the carrier of X)
K6( the carrier of X) is set
s9 is Element of the carrier of S
x2 is (S,x0)
f . s9 is set
f .: x2 is Element of K6( the carrier of X)
f /. s9 is Element of the carrier of X
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
x0 is Element of the carrier of S
{x0} is non empty set
p is (S,x0)
(dom f) /\ p is Element of K6( the carrier of S)
f /. x0 is Element of the carrier of X
x1 is (X,f /. x0)
x2 is (S,x0)
f .: x2 is Element of K6( the carrier of X)
K6( the carrier of X) is set
Im (f,x0) is set
f .: {x0} is set
f . x0 is set
{(f . x0)} is non empty set
{(f /. x0)} is non empty set
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of X, the carrier of S) is set
K6(K7( the carrier of X, the carrier of S)) is set
f is Relation-like the carrier of X -defined the carrier of S -valued Function-like Element of K6(K7( the carrier of X, the carrier of S))
dom f is Element of K6( the carrier of X)
K6( the carrier of X) is set
x0 is Relation-like the carrier of X -defined the carrier of S -valued Function-like Element of K6(K7( the carrier of X, the carrier of S))
dom x0 is Element of K6( the carrier of X)
(dom f) /\ (dom x0) is Element of K6( the carrier of X)
f + x0 is Relation-like the carrier of X -defined the carrier of S -valued Function-like Element of K6(K7( the carrier of X, the carrier of S))
f - x0 is Relation-like the carrier of X -defined the carrier of S -valued Function-like Element of K6(K7( the carrier of X, the carrier of S))
p is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
rng p is Element of K6( the carrier of X)
(f + x0) /* p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
f /* p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
x0 /* p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
(f /* p) + (x0 /* p) is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
(f - x0) /* p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
(f /* p) - (x0 /* p) is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
dom (f + x0) is Element of K6( the carrier of X)
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
p . x1 is Element of the carrier of X
((f + x0) /* p) . x1 is Element of the carrier of S
(f + x0) /. (p . x1) is Element of the carrier of S
f /. (p . x1) is Element of the carrier of S
x0 /. (p . x1) is Element of the carrier of S
(f /. (p . x1)) + (x0 /. (p . x1)) is Element of the carrier of S
(f /* p) . x1 is Element of the carrier of S
((f /* p) . x1) + (x0 /. (p . x1)) is Element of the carrier of S
(x0 /* p) . x1 is Element of the carrier of S
((f /* p) . x1) + ((x0 /* p) . x1) is Element of the carrier of S
dom (f - x0) is Element of K6( the carrier of X)
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
p . x1 is Element of the carrier of X
((f - x0) /* p) . x1 is Element of the carrier of S
(f - x0) /. (p . x1) is Element of the carrier of S
f /. (p . x1) is Element of the carrier of S
x0 /. (p . x1) is Element of the carrier of S
(f /. (p . x1)) - (x0 /. (p . x1)) is Element of the carrier of S
- (x0 /. (p . x1)) is Element of the carrier of S
(f /. (p . x1)) + (- (x0 /. (p . x1))) is Element of the carrier of S
(f /* p) . x1 is Element of the carrier of S
((f /* p) . x1) - (x0 /. (p . x1)) is Element of the carrier of S
((f /* p) . x1) + (- (x0 /. (p . x1))) is Element of the carrier of S
(x0 /* p) . x1 is Element of the carrier of S
((f /* p) . x1) - ((x0 /* p) . x1) is Element of the carrier of S
- ((x0 /* p) . x1) is Element of the carrier of S
((f /* p) . x1) + (- ((x0 /* p) . x1)) is Element of the carrier of S
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of X, the carrier of S) is set
K6(K7( the carrier of X, the carrier of S)) is set
f is Relation-like the carrier of X -defined the carrier of S -valued Function-like Element of K6(K7( the carrier of X, the carrier of S))
dom f is Element of K6( the carrier of X)
K6( the carrier of X) is set
x0 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
rng x0 is Element of K6( the carrier of X)
f /* x0 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
p is V11() real ext-real Element of REAL
p (#) f is Relation-like the carrier of X -defined the carrier of S -valued Function-like Element of K6(K7( the carrier of X, the carrier of S))
(p (#) f) /* x0 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
p * (f /* x0) is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
dom (p (#) f) is Element of K6( the carrier of X)
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x0 . x1 is Element of the carrier of X
((p (#) f) /* x0) . x1 is Element of the carrier of S
(p (#) f) /. (x0 . x1) is Element of the carrier of S
f /. (x0 . x1) is Element of the carrier of S
p * (f /. (x0 . x1)) is Element of the carrier of S
(f /* x0) . x1 is Element of the carrier of S
p * ((f /* x0) . x1) is Element of the carrier of S
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of X, the carrier of S) is set
K6(K7( the carrier of X, the carrier of S)) is set
f is Relation-like the carrier of X -defined the carrier of S -valued Function-like Element of K6(K7( the carrier of X, the carrier of S))
dom f is Element of K6( the carrier of X)
K6( the carrier of X) is set
||.f.|| is Relation-like the carrier of X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of X,REAL))
K7( the carrier of X,REAL) is set
K6(K7( the carrier of X,REAL)) is set
- f is Relation-like the carrier of X -defined the carrier of S -valued Function-like Element of K6(K7( the carrier of X, the carrier of S))
x0 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
rng x0 is Element of K6( the carrier of X)
f /* x0 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
||.(f /* x0).|| is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
||.f.|| /* x0 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
- (f /* x0) is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
(- f) /* x0 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
dom ||.f.|| is Element of K6( the carrier of X)
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x0 . p is Element of the carrier of X
||.(f /* x0).|| . p is V11() real ext-real Element of REAL
(f /* x0) . p is Element of the carrier of S
||.((f /* x0) . p).|| is V11() real ext-real Element of REAL
f /. (x0 . p) is Element of the carrier of S
||.(f /. (x0 . p)).|| is V11() real ext-real Element of REAL
||.f.|| . (x0 . p) is V11() real ext-real Element of REAL
||.f.|| /. (x0 . p) is V11() real ext-real Element of REAL
(||.f.|| /* x0) . p is V11() real ext-real Element of REAL
(- 1) * (f /* x0) is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
(- 1) (#) f is Relation-like the carrier of X -defined the carrier of S -valued Function-like Element of K6(K7( the carrier of X, the carrier of S))
((- 1) (#) f) /* x0 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
x0 is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
f + x0 is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
f - x0 is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
p is Element of the carrier of S
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
dom x0 is Element of K6( the carrier of S)
(dom f) /\ (dom x0) is Element of K6( the carrier of S)
dom (f + x0) is Element of K6( the carrier of S)
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
x1 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
rng x1 is Element of K6( the carrier of S)
lim x1 is Element of the carrier of S
x0 /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
f /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
(f /* x1) + (x0 /* x1) is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
(f + x0) /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
f /. p is Element of the carrier of X
lim (f /* x1) is Element of the carrier of X
x0 /. p is Element of the carrier of X
lim (x0 /* x1) is Element of the carrier of X
(f + x0) /. p is Element of the carrier of X
(f /. p) + (x0 /. p) is Element of the carrier of X
lim ((f /* x1) + (x0 /* x1)) is Element of the carrier of X
lim ((f + x0) /* x1) is Element of the carrier of X
dom (f - x0) is Element of K6( the carrier of S)
x1 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
rng x1 is Element of K6( the carrier of S)
lim x1 is Element of the carrier of S
x0 /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
f /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
(f /* x1) - (x0 /* x1) is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
(f - x0) /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
lim (f /* x1) is Element of the carrier of X
lim (x0 /* x1) is Element of the carrier of X
(f - x0) /. p is Element of the carrier of X
(f /. p) - (x0 /. p) is Element of the carrier of X
- (x0 /. p) is Element of the carrier of X
(f /. p) + (- (x0 /. p)) is Element of the carrier of X
lim ((f /* x1) - (x0 /* x1)) is Element of the carrier of X
lim ((f - x0) /* x1) is Element of the carrier of X
X is V11() real ext-real Element of REAL
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
f is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K7( the carrier of f, the carrier of S) is set
K6(K7( the carrier of f, the carrier of S)) is set
x0 is Relation-like the carrier of f -defined the carrier of S -valued Function-like Element of K6(K7( the carrier of f, the carrier of S))
X (#) x0 is Relation-like the carrier of f -defined the carrier of S -valued Function-like Element of K6(K7( the carrier of f, the carrier of S))
p is Element of the carrier of f
dom x0 is Element of K6( the carrier of f)
K6( the carrier of f) is set
dom (X (#) x0) is Element of K6( the carrier of f)
K7(NAT, the carrier of f) is set
K6(K7(NAT, the carrier of f)) is set
(X (#) x0) /. p is Element of the carrier of S
x1 is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of f))
rng x1 is Element of K6( the carrier of f)
lim x1 is Element of the carrier of f
(X (#) x0) /* x1 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
lim ((X (#) x0) /* x1) is Element of the carrier of S
x0 /. p is Element of the carrier of S
x0 /* x1 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
lim (x0 /* x1) is Element of the carrier of S
X * (x0 /* x1) is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
X * (x0 /. p) is Element of the carrier of S
lim (X * (x0 /* x1)) is Element of the carrier of S
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
||.f.|| is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
K7( the carrier of S,REAL) is set
K6(K7( the carrier of S,REAL)) is set
- f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
x0 is Element of the carrier of S
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
dom ||.f.|| is Element of K6( the carrier of S)
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
rng p is Element of K6( the carrier of S)
lim p is Element of the carrier of S
f /. x0 is Element of the carrier of X
f /* p is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
lim (f /* p) is Element of the carrier of X
||.(f /* p).|| is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
||.f.|| /* p is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
||.f.|| /. x0 is V11() real ext-real Element of REAL
||.f.|| . x0 is V11() real ext-real Element of REAL
||.(f /. x0).|| is V11() real ext-real Element of REAL
lim ||.(f /* p).|| is V11() real ext-real Element of REAL
lim (||.f.|| /* p) is V11() real ext-real Element of REAL
(- 1) (#) f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of X, the carrier of S) is set
K6(K7( the carrier of X, the carrier of S)) is set
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K7( the carrier of X,REAL) is set
K6(K7( the carrier of X,REAL)) is set
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
f is set
x0 is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom x0 is Element of K6( the carrier of S)
K6( the carrier of S) is set
p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
rng p is Element of K6( the carrier of S)
lim p is Element of the carrier of S
x0 | f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom (x0 | f) is Element of K6( the carrier of S)
(dom x0) /\ f is Element of K6( the carrier of S)
dom p is Element of K6(NAT)
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
p . x1 is Element of the carrier of S
(x0 | f) /* p is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
((x0 | f) /* p) . x1 is Element of the carrier of X
(x0 | f) /. (p . x1) is Element of the carrier of X
x0 /. (p . x1) is Element of the carrier of X
x0 /* p is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
(x0 /* p) . x1 is Element of the carrier of X
x0 /. (lim p) is Element of the carrier of X
(x0 | f) /. (lim p) is Element of the carrier of X
lim (x0 /* p) is Element of the carrier of X
p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
rng p is Element of K6( the carrier of S)
lim p is Element of the carrier of S
x0 /* p is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
x0 /. (lim p) is Element of the carrier of X
lim (x0 /* p) is Element of the carrier of X
x0 | f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom (x0 | f) is Element of K6( the carrier of S)
(dom x0) /\ f is Element of K6( the carrier of S)
p is Element of the carrier of S
x1 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
rng x1 is Element of K6( the carrier of S)
lim x1 is Element of the carrier of S
dom x1 is Element of K6(NAT)
x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x1 . x2 is Element of the carrier of S
(x0 | f) /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
((x0 | f) /* x1) . x2 is Element of the carrier of X
(x0 | f) /. (x1 . x2) is Element of the carrier of X
x0 /. (x1 . x2) is Element of the carrier of X
x0 /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
(x0 /* x1) . x2 is Element of the carrier of X
(x0 | f) /. (lim x1) is Element of the carrier of X
x0 /. (lim x1) is Element of the carrier of X
lim ((x0 | f) /* x1) is Element of the carrier of X
(x0 | f) /. p is Element of the carrier of X
X is set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
f is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K7( the carrier of f, the carrier of S) is set
K6(K7( the carrier of f, the carrier of S)) is set
x0 is Relation-like the carrier of f -defined the carrier of S -valued Function-like Element of K6(K7( the carrier of f, the carrier of S))
dom x0 is Element of K6( the carrier of f)
K6( the carrier of f) is set
p is Element of the carrier of f
x0 /. p is Element of the carrier of S
x1 is V11() real ext-real Element of REAL
x0 | X is Relation-like the carrier of f -defined the carrier of S -valued Function-like Element of K6(K7( the carrier of f, the carrier of S))
dom (x0 | X) is Element of K6( the carrier of f)
(x0 | X) /. p is Element of the carrier of S
x2 is V11() real ext-real Element of REAL
s9 is Element of the carrier of f
s9 - p is Element of the carrier of f
- p is Element of the carrier of f
s9 + (- p) is Element of the carrier of f
||.(s9 - p).|| is V11() real ext-real Element of REAL
x0 /. s9 is Element of the carrier of S
(x0 /. s9) - (x0 /. p) is Element of the carrier of S
- (x0 /. p) is Element of the carrier of S
(x0 /. s9) + (- (x0 /. p)) is Element of the carrier of S
||.((x0 /. s9) - (x0 /. p)).|| is V11() real ext-real Element of REAL
(dom x0) /\ X is Element of K6( the carrier of f)
(x0 | X) /. s9 is Element of the carrier of S
((x0 | X) /. s9) - (x0 /. p) is Element of the carrier of S
((x0 | X) /. s9) + (- (x0 /. p)) is Element of the carrier of S
||.(((x0 | X) /. s9) - (x0 /. p)).|| is V11() real ext-real Element of REAL
((x0 | X) /. s9) - ((x0 | X) /. p) is Element of the carrier of S
- ((x0 | X) /. p) is Element of the carrier of S
((x0 | X) /. s9) + (- ((x0 | X) /. p)) is Element of the carrier of S
||.(((x0 | X) /. s9) - ((x0 | X) /. p)).|| is V11() real ext-real Element of REAL
x0 | X is Relation-like the carrier of f -defined the carrier of S -valued Function-like Element of K6(K7( the carrier of f, the carrier of S))
dom (x0 | X) is Element of K6( the carrier of f)
(dom x0) /\ X is Element of K6( the carrier of f)
p is Element of the carrier of f
(x0 | X) /. p is Element of the carrier of S
x1 is V11() real ext-real Element of REAL
x0 /. p is Element of the carrier of S
x2 is V11() real ext-real Element of REAL
s9 is Element of the carrier of f
s9 - p is Element of the carrier of f
- p is Element of the carrier of f
s9 + (- p) is Element of the carrier of f
||.(s9 - p).|| is V11() real ext-real Element of REAL
(x0 | X) /. s9 is Element of the carrier of S
((x0 | X) /. s9) - ((x0 | X) /. p) is Element of the carrier of S
- ((x0 | X) /. p) is Element of the carrier of S
((x0 | X) /. s9) + (- ((x0 | X) /. p)) is Element of the carrier of S
||.(((x0 | X) /. s9) - ((x0 | X) /. p)).|| is V11() real ext-real Element of REAL
((x0 | X) /. s9) - (x0 /. p) is Element of the carrier of S
- (x0 /. p) is Element of the carrier of S
((x0 | X) /. s9) + (- (x0 /. p)) is Element of the carrier of S
||.(((x0 | X) /. s9) - (x0 /. p)).|| is V11() real ext-real Element of REAL
x0 /. s9 is Element of the carrier of S
(x0 /. s9) - (x0 /. p) is Element of the carrier of S
(x0 /. s9) + (- (x0 /. p)) is Element of the carrier of S
||.((x0 /. s9) - (x0 /. p)).|| is V11() real ext-real Element of REAL
X is set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S,REAL) is set
K6(K7( the carrier of S,REAL)) is set
f is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
x0 is Element of the carrier of S
f /. x0 is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
f | X is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
dom (f | X) is Element of K6( the carrier of S)
(f | X) /. x0 is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
x2 is Element of the carrier of S
x2 - x0 is Element of the carrier of S
- x0 is Element of the carrier of S
x2 + (- x0) is Element of the carrier of S
||.(x2 - x0).|| is V11() real ext-real Element of REAL
f /. x2 is V11() real ext-real Element of REAL
(f /. x2) - (f /. x0) is V11() real ext-real Element of REAL
abs ((f /. x2) - (f /. x0)) is V11() real ext-real Element of REAL
(dom f) /\ X is Element of K6( the carrier of S)
(f | X) /. x2 is V11() real ext-real Element of REAL
((f | X) /. x2) - (f /. x0) is V11() real ext-real Element of REAL
abs (((f | X) /. x2) - (f /. x0)) is V11() real ext-real Element of REAL
((f | X) /. x2) - ((f | X) /. x0) is V11() real ext-real Element of REAL
abs (((f | X) /. x2) - ((f | X) /. x0)) is V11() real ext-real Element of REAL
f | X is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
dom (f | X) is Element of K6( the carrier of S)
(dom f) /\ X is Element of K6( the carrier of S)
x0 is Element of the carrier of S
(f | X) /. x0 is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
f /. x0 is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
x2 is Element of the carrier of S
x2 - x0 is Element of the carrier of S
- x0 is Element of the carrier of S
x2 + (- x0) is Element of the carrier of S
||.(x2 - x0).|| is V11() real ext-real Element of REAL
(f | X) /. x2 is V11() real ext-real Element of REAL
((f | X) /. x2) - ((f | X) /. x0) is V11() real ext-real Element of REAL
abs (((f | X) /. x2) - ((f | X) /. x0)) is V11() real ext-real Element of REAL
((f | X) /. x2) - (f /. x0) is V11() real ext-real Element of REAL
abs (((f | X) /. x2) - (f /. x0)) is V11() real ext-real Element of REAL
f /. x2 is V11() real ext-real Element of REAL
(f /. x2) - (f /. x0) is V11() real ext-real Element of REAL
abs ((f /. x2) - (f /. x0)) is V11() real ext-real Element of REAL
X is set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
f is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K7( the carrier of S, the carrier of f) is set
K6(K7( the carrier of S, the carrier of f)) is set
x0 is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
x0 | X is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
dom x0 is Element of K6( the carrier of S)
K6( the carrier of S) is set
(dom x0) /\ X is Element of K6( the carrier of S)
dom (x0 | X) is Element of K6( the carrier of S)
(x0 | X) | X is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
p is Element of the carrier of S
dom (x0 | X) is Element of K6( the carrier of S)
K6( the carrier of S) is set
dom x0 is Element of K6( the carrier of S)
(dom x0) /\ X is Element of K6( the carrier of S)
p is Element of the carrier of S
(x0 | X) | X is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
X is set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S,REAL) is set
K6(K7( the carrier of S,REAL)) is set
f is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
f | X is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
(dom f) /\ X is Element of K6( the carrier of S)
dom (f | X) is Element of K6( the carrier of S)
(f | X) | X is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
x0 is Element of the carrier of S
dom (f | X) is Element of K6( the carrier of S)
K6( the carrier of S) is set
dom f is Element of K6( the carrier of S)
(dom f) /\ X is Element of K6( the carrier of S)
x0 is Element of the carrier of S
(f | X) | X is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
X is set
S is set
f is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of f is non empty set
x0 is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of x0 is non empty set
K7( the carrier of f, the carrier of x0) is set
K6(K7( the carrier of f, the carrier of x0)) is set
p is Relation-like the carrier of f -defined the carrier of x0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of x0))
dom p is Element of K6( the carrier of f)
K6( the carrier of f) is set
p | S is Relation-like the carrier of f -defined the carrier of x0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of x0))
x1 is Element of the carrier of f
p | X is Relation-like the carrier of f -defined the carrier of x0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of x0))
(dom p) /\ S is Element of K6( the carrier of f)
(dom p) /\ X is Element of K6( the carrier of f)
dom (p | S) is Element of K6( the carrier of f)
dom (p | X) is Element of K6( the carrier of f)
K7(NAT, the carrier of f) is set
K6(K7(NAT, the carrier of f)) is set
(p | S) /. x1 is Element of the carrier of x0
(p | X) /. x1 is Element of the carrier of x0
p /. x1 is Element of the carrier of x0
x2 is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of f))
rng x2 is Element of K6( the carrier of f)
lim x2 is Element of the carrier of f
(p | S) /* x2 is non empty Relation-like NAT -defined the carrier of x0 -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of x0))
K7(NAT, the carrier of x0) is set
K6(K7(NAT, the carrier of x0)) is set
lim ((p | S) /* x2) is Element of the carrier of x0
dom x2 is Element of K6(NAT)
s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x2 . s9 is Element of the carrier of f
(p | X) /* x2 is non empty Relation-like NAT -defined the carrier of x0 -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of x0))
((p | X) /* x2) . s9 is Element of the carrier of x0
(p | X) /. (x2 . s9) is Element of the carrier of x0
p /. (x2 . s9) is Element of the carrier of x0
(p | S) /. (x2 . s9) is Element of the carrier of x0
((p | S) /* x2) . s9 is Element of the carrier of x0
lim ((p | X) /* x2) is Element of the carrier of x0
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
x0 is Element of the carrier of S
{x0} is non empty set
p is set
f | {x0} is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
p is Element of the carrier of S
(dom f) /\ {x0} is Element of K6( the carrier of S)
dom (f | {x0}) is Element of K6( the carrier of S)
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
(f | {x0}) /. p is Element of the carrier of X
x1 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
rng x1 is Element of K6( the carrier of S)
lim x1 is Element of the carrier of S
(f | {x0}) /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
lim ((f | {x0}) /* x1) is Element of the carrier of X
dom x1 is Element of K6(NAT)
x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x1 . x2 is Element of the carrier of S
x2 is V11() real ext-real Element of REAL
s9 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non negative Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
((f | {x0}) /* x1) . x1 is Element of the carrier of X
(((f | {x0}) /* x1) . x1) - ((f | {x0}) /. p) is Element of the carrier of X
- ((f | {x0}) /. p) is Element of the carrier of X
(((f | {x0}) /* x1) . x1) + (- ((f | {x0}) /. p)) is Element of the carrier of X
||.((((f | {x0}) /* x1) . x1) - ((f | {x0}) /. p)).|| is V11() real ext-real Element of REAL
x1 . x1 is Element of the carrier of S
(f | {x0}) /. (x1 . x1) is Element of the carrier of X
(f | {x0}) /. x0 is Element of the carrier of X
((f | {x0}) /. (x1 . x1)) - ((f | {x0}) /. x0) is Element of the carrier of X
- ((f | {x0}) /. x0) is Element of the carrier of X
((f | {x0}) /. (x1 . x1)) + (- ((f | {x0}) /. x0)) is Element of the carrier of X
||.(((f | {x0}) /. (x1 . x1)) - ((f | {x0}) /. x0)).|| is V11() real ext-real Element of REAL
((f | {x0}) /. x0) - ((f | {x0}) /. x0) is Element of the carrier of X
((f | {x0}) /. x0) + (- ((f | {x0}) /. x0)) is Element of the carrier of X
||.(((f | {x0}) /. x0) - ((f | {x0}) /. x0)).|| is V11() real ext-real Element of REAL
0. X is V91(X) Element of the carrier of X
||.(0. X).|| is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
f is set
x0 is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
p is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
x0 + p is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
x0 - p is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom x0 is Element of K6( the carrier of S)
K6( the carrier of S) is set
dom p is Element of K6( the carrier of S)
(dom x0) /\ (dom p) is Element of K6( the carrier of S)
dom (x0 + p) is Element of K6( the carrier of S)
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
x1 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
rng x1 is Element of K6( the carrier of S)
lim x1 is Element of the carrier of S
x0 /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
p /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
(x0 /* x1) + (p /* x1) is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
x0 /. (lim x1) is Element of the carrier of X
lim (x0 /* x1) is Element of the carrier of X
p /. (lim x1) is Element of the carrier of X
lim (p /* x1) is Element of the carrier of X
(x0 + p) /. (lim x1) is Element of the carrier of X
(lim (x0 /* x1)) + (lim (p /* x1)) is Element of the carrier of X
lim ((x0 /* x1) + (p /* x1)) is Element of the carrier of X
(x0 + p) /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
lim ((x0 + p) /* x1) is Element of the carrier of X
dom (x0 - p) is Element of K6( the carrier of S)
x1 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
rng x1 is Element of K6( the carrier of S)
lim x1 is Element of the carrier of S
x0 /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
p /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
(x0 /* x1) - (p /* x1) is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
x0 /. (lim x1) is Element of the carrier of X
lim (x0 /* x1) is Element of the carrier of X
p /. (lim x1) is Element of the carrier of X
lim (p /* x1) is Element of the carrier of X
(x0 - p) /. (lim x1) is Element of the carrier of X
(lim (x0 /* x1)) - (lim (p /* x1)) is Element of the carrier of X
- (lim (p /* x1)) is Element of the carrier of X
(lim (x0 /* x1)) + (- (lim (p /* x1))) is Element of the carrier of X
lim ((x0 /* x1) - (p /* x1)) is Element of the carrier of X
(x0 - p) /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
lim ((x0 - p) /* x1) is Element of the carrier of X
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
f is set
x0 is set
f /\ x0 is set
p is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
x1 is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
p + x1 is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
p - x1 is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
f is V11() real ext-real Element of REAL
x0 is set
p is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
f (#) p is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom p is Element of K6( the carrier of S)
K6( the carrier of S) is set
dom (f (#) p) is Element of K6( the carrier of S)
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
x1 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
rng x1 is Element of K6( the carrier of S)
lim x1 is Element of the carrier of S
p /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
f * (p /* x1) is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
p /. (lim x1) is Element of the carrier of X
lim (p /* x1) is Element of the carrier of X
(f (#) p) /. (lim x1) is Element of the carrier of X
f * (lim (p /* x1)) is Element of the carrier of X
lim (f * (p /* x1)) is Element of the carrier of X
(f (#) p) /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
lim ((f (#) p) /* x1) is Element of the carrier of X
X is set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
f is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K7( the carrier of S, the carrier of f) is set
K6(K7( the carrier of S, the carrier of f)) is set
x0 is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
||.x0.|| is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
K7( the carrier of S,REAL) is set
K6(K7( the carrier of S,REAL)) is set
- x0 is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
dom x0 is Element of K6( the carrier of S)
K6( the carrier of S) is set
dom ||.x0.|| is Element of K6( the carrier of S)
||.x0.|| | X is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
p is Element of the carrier of S
x0 | X is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
(dom ||.x0.||) /\ X is Element of K6( the carrier of S)
dom (||.x0.|| | X) is Element of K6( the carrier of S)
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
(||.x0.|| | X) /. p is V11() real ext-real Element of REAL
x1 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
rng x1 is Element of K6( the carrier of S)
lim x1 is Element of the carrier of S
(||.x0.|| | X) /* x1 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim ((||.x0.|| | X) /* x1) is V11() real ext-real Element of REAL
(dom x0) /\ X is Element of K6( the carrier of S)
dom (x0 | X) is Element of K6( the carrier of S)
(x0 | X) /. p is Element of the carrier of f
(x0 | X) /* x1 is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of f))
K7(NAT, the carrier of f) is set
K6(K7(NAT, the carrier of f)) is set
lim ((x0 | X) /* x1) is Element of the carrier of f
dom x1 is Element of K6(NAT)
x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x1 . x2 is Element of the carrier of S
||.((x0 | X) /* x1).|| is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
||.((x0 | X) /* x1).|| . x2 is V11() real ext-real Element of REAL
((x0 | X) /* x1) . x2 is Element of the carrier of f
||.(((x0 | X) /* x1) . x2).|| is V11() real ext-real Element of REAL
(x0 | X) /. (x1 . x2) is Element of the carrier of f
||.((x0 | X) /. (x1 . x2)).|| is V11() real ext-real Element of REAL
x0 /. (x1 . x2) is Element of the carrier of f
||.(x0 /. (x1 . x2)).|| is V11() real ext-real Element of REAL
||.x0.|| . (x1 . x2) is V11() real ext-real Element of REAL
(||.x0.|| | X) . (x1 . x2) is V11() real ext-real Element of REAL
(||.x0.|| | X) /. (x1 . x2) is V11() real ext-real Element of REAL
((||.x0.|| | X) /* x1) . x2 is V11() real ext-real Element of REAL
||.((x0 | X) /. p).|| is V11() real ext-real Element of REAL
x0 /. p is Element of the carrier of f
||.(x0 /. p).|| is V11() real ext-real Element of REAL
||.x0.|| . p is V11() real ext-real Element of REAL
||.x0.|| /. p is V11() real ext-real Element of REAL
(- 1) (#) x0 is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
x0 is Element of the carrier of S
f /. x0 is Element of the carrier of X
0. X is V91(X) Element of the carrier of X
(f /. x0) + (0. X) is Element of the carrier of X
0. S is V91(S) Element of the carrier of S
x0 + (0. S) is Element of the carrier of S
f /. (x0 + (0. S)) is Element of the carrier of X
f /. (0. S) is Element of the carrier of X
(f /. x0) + (f /. (0. S)) is Element of the carrier of X
p is Element of the carrier of S
- p is Element of the carrier of S
p + (- p) is Element of the carrier of S
f /. (p + (- p)) is Element of the carrier of X
f /. p is Element of the carrier of X
f /. (- p) is Element of the carrier of X
(f /. p) + (f /. (- p)) is Element of the carrier of X
- (f /. p) is Element of the carrier of X
p is Element of the carrier of S
x1 is Element of the carrier of S
p - x1 is Element of the carrier of S
- x1 is Element of the carrier of S
p + (- x1) is Element of the carrier of S
f /. (p - x1) is Element of the carrier of X
f /. p is Element of the carrier of X
f /. (- x1) is Element of the carrier of X
(f /. p) + (f /. (- x1)) is Element of the carrier of X
f /. x1 is Element of the carrier of X
(f /. p) - (f /. x1) is Element of the carrier of X
- (f /. x1) is Element of the carrier of X
(f /. p) + (- (f /. x1)) is Element of the carrier of X
p is Element of the carrier of S
x1 is V11() real ext-real Element of REAL
p - x0 is Element of the carrier of S
- x0 is Element of the carrier of S
p + (- x0) is Element of the carrier of S
s9 is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
x1 is Element of the carrier of S
x1 - p is Element of the carrier of S
- p is Element of the carrier of S
x1 + (- p) is Element of the carrier of S
||.(x1 - p).|| is V11() real ext-real Element of REAL
(p - x0) + x0 is Element of the carrier of S
x0 - x0 is Element of the carrier of S
x0 + (- x0) is Element of the carrier of S
p - (x0 - x0) is Element of the carrier of S
- (x0 - x0) is Element of the carrier of S
p + (- (x0 - x0)) is Element of the carrier of S
p - (0. S) is Element of the carrier of S
- (0. S) is Element of the carrier of S
p + (- (0. S)) is Element of the carrier of S
x1 - (p - x0) is Element of the carrier of S
- (p - x0) is Element of the carrier of S
x1 + (- (p - x0)) is Element of the carrier of S
(x1 - (p - x0)) - x0 is Element of the carrier of S
(x1 - (p - x0)) + (- x0) is Element of the carrier of S
||.((x1 - (p - x0)) - x0).|| is V11() real ext-real Element of REAL
f /. x1 is Element of the carrier of X
f /. p is Element of the carrier of X
(f /. x1) - (f /. p) is Element of the carrier of X
- (f /. p) is Element of the carrier of X
(f /. x1) + (- (f /. p)) is Element of the carrier of X
||.((f /. x1) - (f /. p)).|| is V11() real ext-real Element of REAL
f /. (p - x0) is Element of the carrier of X
(f /. (p - x0)) + (f /. x0) is Element of the carrier of X
(f /. x1) - ((f /. (p - x0)) + (f /. x0)) is Element of the carrier of X
- ((f /. (p - x0)) + (f /. x0)) is Element of the carrier of X
(f /. x1) + (- ((f /. (p - x0)) + (f /. x0))) is Element of the carrier of X
||.((f /. x1) - ((f /. (p - x0)) + (f /. x0))).|| is V11() real ext-real Element of REAL
(f /. x1) - (f /. (p - x0)) is Element of the carrier of X
- (f /. (p - x0)) is Element of the carrier of X
(f /. x1) + (- (f /. (p - x0))) is Element of the carrier of X
((f /. x1) - (f /. (p - x0))) - (f /. x0) is Element of the carrier of X
- (f /. x0) is Element of the carrier of X
((f /. x1) - (f /. (p - x0))) + (- (f /. x0)) is Element of the carrier of X
||.(((f /. x1) - (f /. (p - x0))) - (f /. x0)).|| is V11() real ext-real Element of REAL
f /. (x1 - (p - x0)) is Element of the carrier of X
(f /. (x1 - (p - x0))) - (f /. x0) is Element of the carrier of X
(f /. (x1 - (p - x0))) + (- (f /. x0)) is Element of the carrier of X
||.((f /. (x1 - (p - x0))) - (f /. x0)).|| is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
rng f is Element of K6( the carrier of X)
K6( the carrier of X) is set
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
x0 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
rng x0 is Element of K6( the carrier of X)
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x0 . p is set
dom x0 is Element of K6(NAT)
x0 . p is Element of the carrier of X
x1 is Element of the carrier of S
f . x1 is set
f /. x1 is Element of the carrier of X
K7(NAT, the carrier of S) is set
K6(K7(NAT, the carrier of S)) is set
p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
x1 is set
rng p is Element of K6( the carrier of S)
x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
p . x2 is Element of the carrier of S
x1 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of S))
lim x1 is Element of the carrier of S
f /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
rng x1 is Element of K6( the carrier of S)
s9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
p . s9 is Element of the carrier of S
f /. (p . s9) is Element of the carrier of X
x0 . s9 is Element of the carrier of X
f /* p is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
(f /* p) . s9 is Element of the carrier of X
f | (dom f) is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
f /. (lim x1) is Element of the carrier of X
lim (f /* x1) is Element of the carrier of X
x2 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
lim x2 is Element of the carrier of X
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K7( the carrier of X,REAL) is set
K6(K7( the carrier of X,REAL)) is set
S is Relation-like the carrier of X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of X,REAL))
dom S is Element of K6( the carrier of X)
K6( the carrier of X) is set
rng S is V47() V48() V49() Element of K6(REAL)
f is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng f is V47() V48() V49() Element of K6(REAL)
x0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f . x0 is V11() real ext-real Element of REAL
dom f is Element of K6(NAT)
p is Element of the carrier of X
S . p is V11() real ext-real Element of REAL
S /. p is V11() real ext-real Element of REAL
K7(NAT, the carrier of X) is set
K6(K7(NAT, the carrier of X)) is set
x0 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
p is set
rng x0 is Element of K6( the carrier of X)
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x0 . x1 is Element of the carrier of X
p is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of X))
lim p is Element of the carrier of X
S /* p is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng p is Element of K6( the carrier of X)
x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
x0 . x2 is Element of the carrier of X
S /. (x0 . x2) is V11() real ext-real Element of REAL
f . x2 is V11() real ext-real Element of REAL
S /* x0 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(S /* x0) . x2 is V11() real ext-real Element of REAL
S | (dom S) is Relation-like the carrier of X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of X,REAL))
S /. (lim p) is V11() real ext-real Element of REAL
lim (S /* p) is V11() real ext-real Element of REAL
x1 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
lim x1 is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
K6( the carrier of S) is set
f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom f is Element of K6( the carrier of S)
x0 is Element of K6( the carrier of S)
f .: x0 is Element of K6( the carrier of X)
K6( the carrier of X) is set
f | x0 is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom (f | x0) is Element of K6( the carrier of S)
(dom f) /\ x0 is Element of K6( the carrier of S)
(f | x0) | x0 is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
p is Element of the carrier of S
rng (f | x0) is Element of K6( the carrier of X)
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K7( the carrier of X,REAL) is set
K6(K7( the carrier of X,REAL)) is set
S is Relation-like the carrier of X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of X,REAL))
dom S is Element of K6( the carrier of X)
K6( the carrier of X) is set
rng S is V47() V48() V49() Element of K6(REAL)
upper_bound (rng S) is V11() real ext-real Element of REAL
lower_bound (rng S) is V11() real ext-real Element of REAL
f is Element of the carrier of X
S . f is V11() real ext-real Element of REAL
S /. f is V11() real ext-real Element of REAL
x0 is Element of the carrier of X
S . x0 is V11() real ext-real Element of REAL
S /. x0 is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
||.f.|| is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
K7( the carrier of S,REAL) is set
K6(K7( the carrier of S,REAL)) is set
rng ||.f.|| is V47() V48() V49() Element of K6(REAL)
upper_bound (rng ||.f.||) is V11() real ext-real Element of REAL
lower_bound (rng ||.f.||) is V11() real ext-real Element of REAL
dom ||.f.|| is Element of K6( the carrier of S)
x0 is Element of the carrier of S
||.f.|| . x0 is V11() real ext-real Element of REAL
p is Element of the carrier of S
||.f.|| . p is V11() real ext-real Element of REAL
||.f.|| /. x0 is V11() real ext-real Element of REAL
||.f.|| /. p is V11() real ext-real Element of REAL
X is set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
f is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K7( the carrier of S, the carrier of f) is set
K6(K7( the carrier of S, the carrier of f)) is set
x0 is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
||.x0.|| is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
K7( the carrier of S,REAL) is set
K6(K7( the carrier of S,REAL)) is set
||.x0.|| | X is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
x0 | X is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
||.(x0 | X).|| is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
dom (||.x0.|| | X) is Element of K6( the carrier of S)
K6( the carrier of S) is set
dom ||.x0.|| is Element of K6( the carrier of S)
(dom ||.x0.||) /\ X is Element of K6( the carrier of S)
dom x0 is Element of K6( the carrier of S)
(dom x0) /\ X is Element of K6( the carrier of S)
dom (x0 | X) is Element of K6( the carrier of S)
dom ||.(x0 | X).|| is Element of K6( the carrier of S)
p is Element of the carrier of S
(||.x0.|| | X) . p is V11() real ext-real Element of REAL
||.x0.|| . p is V11() real ext-real Element of REAL
x0 /. p is Element of the carrier of f
||.(x0 /. p).|| is V11() real ext-real Element of REAL
(x0 | X) /. p is Element of the carrier of f
||.((x0 | X) /. p).|| is V11() real ext-real Element of REAL
||.(x0 | X).|| . p is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
K6( the carrier of S) is set
f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom f is Element of K6( the carrier of S)
||.f.|| is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
K7( the carrier of S,REAL) is set
K6(K7( the carrier of S,REAL)) is set
x0 is Element of K6( the carrier of S)
||.f.|| .: x0 is V47() V48() V49() Element of K6(REAL)
upper_bound (||.f.|| .: x0) is V11() real ext-real Element of REAL
lower_bound (||.f.|| .: x0) is V11() real ext-real Element of REAL
f | x0 is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
dom (f | x0) is Element of K6( the carrier of S)
(dom f) /\ x0 is Element of K6( the carrier of S)
(f | x0) | x0 is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
p is Element of the carrier of S
||.(f | x0).|| is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
rng ||.(f | x0).|| is V47() V48() V49() Element of K6(REAL)
upper_bound (rng ||.(f | x0).||) is V11() real ext-real Element of REAL
lower_bound (rng ||.(f | x0).||) is V11() real ext-real Element of REAL
p is Element of the carrier of S
x1 is Element of the carrier of S
||.(f | x0).|| /. p is V11() real ext-real Element of REAL
||.(f | x0).|| /. x1 is V11() real ext-real Element of REAL
dom ||.f.|| is Element of K6( the carrier of S)
||.f.|| /. p is V11() real ext-real Element of REAL
||.f.|| /. x1 is V11() real ext-real Element of REAL
||.f.|| | x0 is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
rng (||.f.|| | x0) is V47() V48() V49() Element of K6(REAL)
dom ||.(f | x0).|| is Element of K6( the carrier of S)
||.(f | x0).|| . x1 is V11() real ext-real Element of REAL
(f | x0) /. x1 is Element of the carrier of X
||.((f | x0) /. x1).|| is V11() real ext-real Element of REAL
f /. x1 is Element of the carrier of X
||.(f /. x1).|| is V11() real ext-real Element of REAL
||.f.|| . x1 is V11() real ext-real Element of REAL
||.(f | x0).|| . p is V11() real ext-real Element of REAL
(f | x0) /. p is Element of the carrier of X
||.((f | x0) /. p).|| is V11() real ext-real Element of REAL
f /. p is Element of the carrier of X
||.(f /. p).|| is V11() real ext-real Element of REAL
||.f.|| . p is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K7( the carrier of X,REAL) is set
K6(K7( the carrier of X,REAL)) is set
K6( the carrier of X) is set
S is Relation-like the carrier of X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of X,REAL))
dom S is Element of K6( the carrier of X)
f is Element of K6( the carrier of X)
S .: f is V47() V48() V49() Element of K6(REAL)
upper_bound (S .: f) is V11() real ext-real Element of REAL
lower_bound (S .: f) is V11() real ext-real Element of REAL
S | f is Relation-like the carrier of X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of X,REAL))
dom (S | f) is Element of K6( the carrier of X)
(dom S) /\ f is Element of K6( the carrier of X)
(S | f) | f is Relation-like the carrier of X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of X,REAL))
x0 is Element of the carrier of X
rng (S | f) is V47() V48() V49() Element of K6(REAL)
upper_bound (rng (S | f)) is V11() real ext-real Element of REAL
lower_bound (rng (S | f)) is V11() real ext-real Element of REAL
x0 is Element of the carrier of X
p is Element of the carrier of X
(S | f) /. x0 is V11() real ext-real Element of REAL
(S | f) /. p is V11() real ext-real Element of REAL
S /. x0 is V11() real ext-real Element of REAL
S /. p is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of X, the carrier of S) is set
K6(K7( the carrier of X, the carrier of S)) is set
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K7( the carrier of X,REAL) is set
K6(K7( the carrier of X,REAL)) is set
X is set
S is set
f is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of f is non empty set
x0 is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of x0 is non empty set
K7( the carrier of f, the carrier of x0) is set
K6(K7( the carrier of f, the carrier of x0)) is set
p is Relation-like the carrier of f -defined the carrier of x0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of x0))
dom p is Element of K6( the carrier of f)
K6( the carrier of f) is set
x1 is V11() real ext-real Element of REAL
x2 is Element of the carrier of f
p /. x2 is Element of the carrier of x0
s9 is Element of the carrier of f
p /. s9 is Element of the carrier of x0
(p /. x2) - (p /. s9) is Element of the carrier of x0
- (p /. s9) is Element of the carrier of x0
(p /. x2) + (- (p /. s9)) is Element of the carrier of x0
||.((p /. x2) - (p /. s9)).|| is V11() real ext-real Element of REAL
x2 - s9 is Element of the carrier of f
- s9 is Element of the carrier of f
x2 + (- s9) is Element of the carrier of f
||.(x2 - s9).|| is V11() real ext-real Element of REAL
x1 * ||.(x2 - s9).|| is V11() real ext-real Element of REAL
X is set
S is set
X /\ S is set
f is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of f is non empty set
x0 is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of x0 is non empty set
K7( the carrier of f, the carrier of x0) is set
K6(K7( the carrier of f, the carrier of x0)) is set
p is Relation-like the carrier of f -defined the carrier of x0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of x0))
x1 is Relation-like the carrier of f -defined the carrier of x0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of x0))
p + x1 is Relation-like the carrier of f -defined the carrier of x0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of x0))
x2 is V11() real ext-real Element of REAL
dom x1 is Element of K6( the carrier of f)
K6( the carrier of f) is set
dom p is Element of K6( the carrier of f)
(dom p) /\ (dom x1) is Element of K6( the carrier of f)
dom (p + x1) is Element of K6( the carrier of f)
s9 is V11() real ext-real Element of REAL
x2 + s9 is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
0 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of REAL
x1 is Element of the carrier of f
(p + x1) /. x1 is Element of the carrier of x0
x2 is Element of the carrier of f
(p + x1) /. x2 is Element of the carrier of x0
((p + x1) /. x1) - ((p + x1) /. x2) is Element of the carrier of x0
- ((p + x1) /. x2) is Element of the carrier of x0
((p + x1) /. x1) + (- ((p + x1) /. x2)) is Element of the carrier of x0
||.(((p + x1) /. x1) - ((p + x1) /. x2)).|| is V11() real ext-real Element of REAL
x1 - x2 is Element of the carrier of f
- x2 is Element of the carrier of f
x1 + (- x2) is Element of the carrier of f
||.(x1 - x2).|| is V11() real ext-real Element of REAL
x1 * ||.(x1 - x2).|| is V11() real ext-real Element of REAL
x1 /. x1 is Element of the carrier of x0
x1 /. x2 is Element of the carrier of x0
(x1 /. x1) - (x1 /. x2) is Element of the carrier of x0
- (x1 /. x2) is Element of the carrier of x0
(x1 /. x1) + (- (x1 /. x2)) is Element of the carrier of x0
||.((x1 /. x1) - (x1 /. x2)).|| is V11() real ext-real Element of REAL
s9 * ||.(x1 - x2).|| is V11() real ext-real Element of REAL
p /. x1 is Element of the carrier of x0
p /. x2 is Element of the carrier of x0
(p /. x1) - (p /. x2) is Element of the carrier of x0
- (p /. x2) is Element of the carrier of x0
(p /. x1) + (- (p /. x2)) is Element of the carrier of x0
||.((p /. x1) - (p /. x2)).|| is V11() real ext-real Element of REAL
x2 * ||.(x1 - x2).|| is V11() real ext-real Element of REAL
||.((p /. x1) - (p /. x2)).|| + ||.((x1 /. x1) - (x1 /. x2)).|| is V11() real ext-real Element of REAL
(x2 * ||.(x1 - x2).||) + (s9 * ||.(x1 - x2).||) is V11() real ext-real Element of REAL
(p /. x1) + (x1 /. x1) is Element of the carrier of x0
((p /. x1) + (x1 /. x1)) - ((p + x1) /. x2) is Element of the carrier of x0
((p /. x1) + (x1 /. x1)) + (- ((p + x1) /. x2)) is Element of the carrier of x0
||.(((p /. x1) + (x1 /. x1)) - ((p + x1) /. x2)).|| is V11() real ext-real Element of REAL
(p /. x2) + (x1 /. x2) is Element of the carrier of x0
((p /. x1) + (x1 /. x1)) - ((p /. x2) + (x1 /. x2)) is Element of the carrier of x0
- ((p /. x2) + (x1 /. x2)) is Element of the carrier of x0
((p /. x1) + (x1 /. x1)) + (- ((p /. x2) + (x1 /. x2))) is Element of the carrier of x0
||.(((p /. x1) + (x1 /. x1)) - ((p /. x2) + (x1 /. x2))).|| is V11() real ext-real Element of REAL
(x1 /. x1) - ((p /. x2) + (x1 /. x2)) is Element of the carrier of x0
(x1 /. x1) + (- ((p /. x2) + (x1 /. x2))) is Element of the carrier of x0
(p /. x1) + ((x1 /. x1) - ((p /. x2) + (x1 /. x2))) is Element of the carrier of x0
||.((p /. x1) + ((x1 /. x1) - ((p /. x2) + (x1 /. x2)))).|| is V11() real ext-real Element of REAL
(x1 /. x1) - (p /. x2) is Element of the carrier of x0
(x1 /. x1) + (- (p /. x2)) is Element of the carrier of x0
((x1 /. x1) - (p /. x2)) - (x1 /. x2) is Element of the carrier of x0
((x1 /. x1) - (p /. x2)) + (- (x1 /. x2)) is Element of the carrier of x0
(p /. x1) + (((x1 /. x1) - (p /. x2)) - (x1 /. x2)) is Element of the carrier of x0
||.((p /. x1) + (((x1 /. x1) - (p /. x2)) - (x1 /. x2))).|| is V11() real ext-real Element of REAL
(- (p /. x2)) + (x1 /. x1) is Element of the carrier of x0
((- (p /. x2)) + (x1 /. x1)) - (x1 /. x2) is Element of the carrier of x0
((- (p /. x2)) + (x1 /. x1)) + (- (x1 /. x2)) is Element of the carrier of x0
(p /. x1) + (((- (p /. x2)) + (x1 /. x1)) - (x1 /. x2)) is Element of the carrier of x0
||.((p /. x1) + (((- (p /. x2)) + (x1 /. x1)) - (x1 /. x2))).|| is V11() real ext-real Element of REAL
(- (p /. x2)) + ((x1 /. x1) - (x1 /. x2)) is Element of the carrier of x0
(p /. x1) + ((- (p /. x2)) + ((x1 /. x1) - (x1 /. x2))) is Element of the carrier of x0
||.((p /. x1) + ((- (p /. x2)) + ((x1 /. x1) - (x1 /. x2)))).|| is V11() real ext-real Element of REAL
((p /. x1) - (p /. x2)) + ((x1 /. x1) - (x1 /. x2)) is Element of the carrier of x0
||.(((p /. x1) - (p /. x2)) + ((x1 /. x1) - (x1 /. x2))).|| is V11() real ext-real Element of REAL
X is set
S is set
X /\ S is set
f is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of f is non empty set
x0 is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of x0 is non empty set
K7( the carrier of f, the carrier of x0) is set
K6(K7( the carrier of f, the carrier of x0)) is set
p is Relation-like the carrier of f -defined the carrier of x0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of x0))
x1 is Relation-like the carrier of f -defined the carrier of x0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of x0))
p - x1 is Relation-like the carrier of f -defined the carrier of x0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of x0))
x2 is V11() real ext-real Element of REAL
dom x1 is Element of K6( the carrier of f)
K6( the carrier of f) is set
dom p is Element of K6( the carrier of f)
(dom p) /\ (dom x1) is Element of K6( the carrier of f)
dom (p - x1) is Element of K6( the carrier of f)
s9 is V11() real ext-real Element of REAL
x2 + s9 is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
0 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of REAL
x1 is Element of the carrier of f
(p - x1) /. x1 is Element of the carrier of x0
x2 is Element of the carrier of f
(p - x1) /. x2 is Element of the carrier of x0
((p - x1) /. x1) - ((p - x1) /. x2) is Element of the carrier of x0
- ((p - x1) /. x2) is Element of the carrier of x0
((p - x1) /. x1) + (- ((p - x1) /. x2)) is Element of the carrier of x0
||.(((p - x1) /. x1) - ((p - x1) /. x2)).|| is V11() real ext-real Element of REAL
x1 - x2 is Element of the carrier of f
- x2 is Element of the carrier of f
x1 + (- x2) is Element of the carrier of f
||.(x1 - x2).|| is V11() real ext-real Element of REAL
x1 * ||.(x1 - x2).|| is V11() real ext-real Element of REAL
x1 /. x1 is Element of the carrier of x0
x1 /. x2 is Element of the carrier of x0
(x1 /. x1) - (x1 /. x2) is Element of the carrier of x0
- (x1 /. x2) is Element of the carrier of x0
(x1 /. x1) + (- (x1 /. x2)) is Element of the carrier of x0
||.((x1 /. x1) - (x1 /. x2)).|| is V11() real ext-real Element of REAL
s9 * ||.(x1 - x2).|| is V11() real ext-real Element of REAL
p /. x1 is Element of the carrier of x0
p /. x2 is Element of the carrier of x0
(p /. x1) - (p /. x2) is Element of the carrier of x0
- (p /. x2) is Element of the carrier of x0
(p /. x1) + (- (p /. x2)) is Element of the carrier of x0
||.((p /. x1) - (p /. x2)).|| is V11() real ext-real Element of REAL
x2 * ||.(x1 - x2).|| is V11() real ext-real Element of REAL
||.((p /. x1) - (p /. x2)).|| + ||.((x1 /. x1) - (x1 /. x2)).|| is V11() real ext-real Element of REAL
(x2 * ||.(x1 - x2).||) + (s9 * ||.(x1 - x2).||) is V11() real ext-real Element of REAL
(p /. x1) - (x1 /. x1) is Element of the carrier of x0
- (x1 /. x1) is Element of the carrier of x0
(p /. x1) + (- (x1 /. x1)) is Element of the carrier of x0
((p /. x1) - (x1 /. x1)) - ((p - x1) /. x2) is Element of the carrier of x0
((p /. x1) - (x1 /. x1)) + (- ((p - x1) /. x2)) is Element of the carrier of x0
||.(((p /. x1) - (x1 /. x1)) - ((p - x1) /. x2)).|| is V11() real ext-real Element of REAL
(p /. x2) - (x1 /. x2) is Element of the carrier of x0
(p /. x2) + (- (x1 /. x2)) is Element of the carrier of x0
((p /. x1) - (x1 /. x1)) - ((p /. x2) - (x1 /. x2)) is Element of the carrier of x0
- ((p /. x2) - (x1 /. x2)) is Element of the carrier of x0
((p /. x1) - (x1 /. x1)) + (- ((p /. x2) - (x1 /. x2))) is Element of the carrier of x0
||.(((p /. x1) - (x1 /. x1)) - ((p /. x2) - (x1 /. x2))).|| is V11() real ext-real Element of REAL
(x1 /. x1) + ((p /. x2) - (x1 /. x2)) is Element of the carrier of x0
(p /. x1) - ((x1 /. x1) + ((p /. x2) - (x1 /. x2))) is Element of the carrier of x0
- ((x1 /. x1) + ((p /. x2) - (x1 /. x2))) is Element of the carrier of x0
(p /. x1) + (- ((x1 /. x1) + ((p /. x2) - (x1 /. x2)))) is Element of the carrier of x0
||.((p /. x1) - ((x1 /. x1) + ((p /. x2) - (x1 /. x2)))).|| is V11() real ext-real Element of REAL
(p /. x2) + (x1 /. x1) is Element of the carrier of x0
((p /. x2) + (x1 /. x1)) - (x1 /. x2) is Element of the carrier of x0
((p /. x2) + (x1 /. x1)) + (- (x1 /. x2)) is Element of the carrier of x0
(p /. x1) - (((p /. x2) + (x1 /. x1)) - (x1 /. x2)) is Element of the carrier of x0
- (((p /. x2) + (x1 /. x1)) - (x1 /. x2)) is Element of the carrier of x0
(p /. x1) + (- (((p /. x2) + (x1 /. x1)) - (x1 /. x2))) is Element of the carrier of x0
||.((p /. x1) - (((p /. x2) + (x1 /. x1)) - (x1 /. x2))).|| is V11() real ext-real Element of REAL
(p /. x2) + ((x1 /. x1) - (x1 /. x2)) is Element of the carrier of x0
(p /. x1) - ((p /. x2) + ((x1 /. x1) - (x1 /. x2))) is Element of the carrier of x0
- ((p /. x2) + ((x1 /. x1) - (x1 /. x2))) is Element of the carrier of x0
(p /. x1) + (- ((p /. x2) + ((x1 /. x1) - (x1 /. x2)))) is Element of the carrier of x0
||.((p /. x1) - ((p /. x2) + ((x1 /. x1) - (x1 /. x2)))).|| is V11() real ext-real Element of REAL
((p /. x1) - (p /. x2)) - ((x1 /. x1) - (x1 /. x2)) is Element of the carrier of x0
- ((x1 /. x1) - (x1 /. x2)) is Element of the carrier of x0
((p /. x1) - (p /. x2)) + (- ((x1 /. x1) - (x1 /. x2))) is Element of the carrier of x0
||.(((p /. x1) - (p /. x2)) - ((x1 /. x1) - (x1 /. x2))).|| is V11() real ext-real Element of REAL
X is set
S is V11() real ext-real Element of REAL
f is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of f is non empty set
x0 is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of x0 is non empty set
K7( the carrier of f, the carrier of x0) is set
K6(K7( the carrier of f, the carrier of x0)) is set
p is Relation-like the carrier of f -defined the carrier of x0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of x0))
S (#) p is Relation-like the carrier of f -defined the carrier of x0 -valued Function-like Element of K6(K7( the carrier of f, the carrier of x0))
x1 is V11() real ext-real Element of REAL
dom p is Element of K6( the carrier of f)
K6( the carrier of f) is set
dom (S (#) p) is Element of K6( the carrier of f)
x2 is V11() real ext-real Element of REAL
s9 is Element of the carrier of f
x1 is Element of the carrier of f
s9 - x1 is Element of the carrier of f
- x1 is Element of the carrier of f
s9 + (- x1) is Element of the carrier of f
||.(s9 - x1).|| is V11() real ext-real Element of REAL
x2 * 0 is V11() real ext-real Element of REAL
x2 * ||.(s9 - x1).|| is V11() real ext-real Element of REAL
(S (#) p) /. s9 is Element of the carrier of x0
(S (#) p) /. x1 is Element of the carrier of x0
((S (#) p) /. s9) - ((S (#) p) /. x1) is Element of the carrier of x0
- ((S (#) p) /. x1) is Element of the carrier of x0
((S (#) p) /. s9) + (- ((S (#) p) /. x1)) is Element of the carrier of x0
||.(((S (#) p) /. s9) - ((S (#) p) /. x1)).|| is V11() real ext-real Element of REAL
p /. s9 is Element of the carrier of x0
S * (p /. s9) is Element of the carrier of x0
(S * (p /. s9)) - ((S (#) p) /. x1) is Element of the carrier of x0
(S * (p /. s9)) + (- ((S (#) p) /. x1)) is Element of the carrier of x0
||.((S * (p /. s9)) - ((S (#) p) /. x1)).|| is V11() real ext-real Element of REAL
0. x0 is V91(x0) Element of the carrier of x0
(0. x0) - ((S (#) p) /. x1) is Element of the carrier of x0
(0. x0) + (- ((S (#) p) /. x1)) is Element of the carrier of x0
||.((0. x0) - ((S (#) p) /. x1)).|| is V11() real ext-real Element of REAL
p /. x1 is Element of the carrier of x0
S * (p /. x1) is Element of the carrier of x0
(0. x0) - (S * (p /. x1)) is Element of the carrier of x0
- (S * (p /. x1)) is Element of the carrier of x0
(0. x0) + (- (S * (p /. x1))) is Element of the carrier of x0
||.((0. x0) - (S * (p /. x1))).|| is V11() real ext-real Element of REAL
(0. x0) - (0. x0) is Element of the carrier of x0
- (0. x0) is Element of the carrier of x0
(0. x0) + (- (0. x0)) is Element of the carrier of x0
||.((0. x0) - (0. x0)).|| is V11() real ext-real Element of REAL
||.(0. x0).|| is V11() real ext-real Element of REAL
abs S is V11() real ext-real Element of REAL
(abs S) * x1 is V11() real ext-real Element of REAL
0 * x1 is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
s9 is Element of the carrier of f
x1 is Element of the carrier of f
p /. s9 is Element of the carrier of x0
p /. x1 is Element of the carrier of x0
(p /. s9) - (p /. x1) is Element of the carrier of x0
- (p /. x1) is Element of the carrier of x0
(p /. s9) + (- (p /. x1)) is Element of the carrier of x0
||.((p /. s9) - (p /. x1)).|| is V11() real ext-real Element of REAL
(abs S) * ||.((p /. s9) - (p /. x1)).|| is V11() real ext-real Element of REAL
s9 - x1 is Element of the carrier of f
- x1 is Element of the carrier of f
s9 + (- x1) is Element of the carrier of f
||.(s9 - x1).|| is V11() real ext-real Element of REAL
x1 * ||.(s9 - x1).|| is V11() real ext-real Element of REAL
(abs S) * (x1 * ||.(s9 - x1).||) is V11() real ext-real Element of REAL
(S (#) p) /. s9 is Element of the carrier of x0
(S (#) p) /. x1 is Element of the carrier of x0
((S (#) p) /. s9) - ((S (#) p) /. x1) is Element of the carrier of x0
- ((S (#) p) /. x1) is Element of the carrier of x0
((S (#) p) /. s9) + (- ((S (#) p) /. x1)) is Element of the carrier of x0
||.(((S (#) p) /. s9) - ((S (#) p) /. x1)).|| is V11() real ext-real Element of REAL
S * (p /. s9) is Element of the carrier of x0
(S * (p /. s9)) - ((S (#) p) /. x1) is Element of the carrier of x0
(S * (p /. s9)) + (- ((S (#) p) /. x1)) is Element of the carrier of x0
||.((S * (p /. s9)) - ((S (#) p) /. x1)).|| is V11() real ext-real Element of REAL
S * (p /. x1) is Element of the carrier of x0
(S * (p /. s9)) - (S * (p /. x1)) is Element of the carrier of x0
- (S * (p /. x1)) is Element of the carrier of x0
(S * (p /. s9)) + (- (S * (p /. x1))) is Element of the carrier of x0
||.((S * (p /. s9)) - (S * (p /. x1))).|| is V11() real ext-real Element of REAL
S * ((p /. s9) - (p /. x1)) is Element of the carrier of x0
||.(S * ((p /. s9) - (p /. x1))).|| is V11() real ext-real Element of REAL
x2 * ||.(s9 - x1).|| is V11() real ext-real Element of REAL
x2 is V11() real ext-real Element of REAL
X is set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
f is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K7( the carrier of S, the carrier of f) is set
K6(K7( the carrier of S, the carrier of f)) is set
x0 is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
- x0 is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
||.x0.|| is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
K7( the carrier of S,REAL) is set
K6(K7( the carrier of S,REAL)) is set
p is V11() real ext-real Element of REAL
(- 1) (#) x0 is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
dom x0 is Element of K6( the carrier of S)
K6( the carrier of S) is set
dom ||.x0.|| is Element of K6( the carrier of S)
x1 is Element of the carrier of S
||.x0.|| /. x1 is V11() real ext-real Element of REAL
x2 is Element of the carrier of S
||.x0.|| /. x2 is V11() real ext-real Element of REAL
(||.x0.|| /. x1) - (||.x0.|| /. x2) is V11() real ext-real Element of REAL
abs ((||.x0.|| /. x1) - (||.x0.|| /. x2)) is V11() real ext-real Element of REAL
x1 - x2 is Element of the carrier of S
- x2 is Element of the carrier of S
x1 + (- x2) is Element of the carrier of S
||.(x1 - x2).|| is V11() real ext-real Element of REAL
p * ||.(x1 - x2).|| is V11() real ext-real Element of REAL
||.x0.|| . x1 is V11() real ext-real Element of REAL
(||.x0.|| . x1) - (||.x0.|| /. x2) is V11() real ext-real Element of REAL
abs ((||.x0.|| . x1) - (||.x0.|| /. x2)) is V11() real ext-real Element of REAL
||.x0.|| . x2 is V11() real ext-real Element of REAL
(||.x0.|| . x1) - (||.x0.|| . x2) is V11() real ext-real Element of REAL
abs ((||.x0.|| . x1) - (||.x0.|| . x2)) is V11() real ext-real Element of REAL
x0 /. x1 is Element of the carrier of f
||.(x0 /. x1).|| is V11() real ext-real Element of REAL
||.(x0 /. x1).|| - (||.x0.|| . x2) is V11() real ext-real Element of REAL
abs (||.(x0 /. x1).|| - (||.x0.|| . x2)) is V11() real ext-real Element of REAL
x0 /. x2 is Element of the carrier of f
||.(x0 /. x2).|| is V11() real ext-real Element of REAL
||.(x0 /. x1).|| - ||.(x0 /. x2).|| is V11() real ext-real Element of REAL
abs (||.(x0 /. x1).|| - ||.(x0 /. x2).||) is V11() real ext-real Element of REAL
(x0 /. x1) - (x0 /. x2) is Element of the carrier of f
- (x0 /. x2) is Element of the carrier of f
(x0 /. x1) + (- (x0 /. x2)) is Element of the carrier of f
||.((x0 /. x1) - (x0 /. x2)).|| is V11() real ext-real Element of REAL
X is set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
f is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K7( the carrier of S, the carrier of f) is set
K6(K7( the carrier of S, the carrier of f)) is set
x0 is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
dom x0 is Element of K6( the carrier of S)
K6( the carrier of S) is set
x0 | X is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
p is Element of the carrier of S
x1 is Element of the carrier of S
X /\ (dom x0) is Element of K6( the carrier of S)
x0 /. p is Element of the carrier of f
x0 . p is set
x0 . x1 is set
x0 /. x1 is Element of the carrier of f
(x0 /. p) - (x0 /. x1) is Element of the carrier of f
- (x0 /. x1) is Element of the carrier of f
(x0 /. p) + (- (x0 /. x1)) is Element of the carrier of f
||.((x0 /. p) - (x0 /. x1)).|| is V11() real ext-real Element of REAL
0. f is V91(f) Element of the carrier of f
||.(0. f).|| is V11() real ext-real Element of REAL
p - x1 is Element of the carrier of S
- x1 is Element of the carrier of S
p + (- x1) is Element of the carrier of S
||.(p - x1).|| is V11() real ext-real Element of REAL
1 * ||.(p - x1).|| is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K6( the carrier of X) is set
S is Element of K6( the carrier of X)
id S is Relation-like the carrier of X -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of X, the carrier of X))
K7( the carrier of X, the carrier of X) is set
K6(K7( the carrier of X, the carrier of X)) is set
dom (id S) is Element of K6( the carrier of X)
f is V11() real ext-real Element of REAL
x0 is Element of the carrier of X
(id S) /. x0 is Element of the carrier of X
p is Element of the carrier of X
(id S) /. p is Element of the carrier of X
((id S) /. x0) - ((id S) /. p) is Element of the carrier of X
- ((id S) /. p) is Element of the carrier of X
((id S) /. x0) + (- ((id S) /. p)) is Element of the carrier of X
||.(((id S) /. x0) - ((id S) /. p)).|| is V11() real ext-real Element of REAL
x0 - p is Element of the carrier of X
- p is Element of the carrier of X
x0 + (- p) is Element of the carrier of X
||.(x0 - p).|| is V11() real ext-real Element of REAL
f * ||.(x0 - p).|| is V11() real ext-real Element of REAL
x0 - ((id S) /. p) is Element of the carrier of X
x0 + (- ((id S) /. p)) is Element of the carrier of X
||.(x0 - ((id S) /. p)).|| is V11() real ext-real Element of REAL
X is set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
f is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K7( the carrier of S, the carrier of f) is set
K6(K7( the carrier of S, the carrier of f)) is set
x0 is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
p is V11() real ext-real Element of REAL
dom x0 is Element of K6( the carrier of S)
K6( the carrier of S) is set
x0 | X is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
dom (x0 | X) is Element of K6( the carrier of S)
x1 is Element of the carrier of S
x2 is V11() real ext-real Element of REAL
x2 / p is V11() real ext-real Element of REAL
x1 is Element of the carrier of S
x1 - x1 is Element of the carrier of S
- x1 is Element of the carrier of S
x1 + (- x1) is Element of the carrier of S
||.(x1 - x1).|| is V11() real ext-real Element of REAL
(x2 / p) * p is V11() real ext-real Element of REAL
p * ||.(x1 - x1).|| is V11() real ext-real Element of REAL
x0 /. x1 is Element of the carrier of f
x0 /. x1 is Element of the carrier of f
(x0 /. x1) - (x0 /. x1) is Element of the carrier of f
- (x0 /. x1) is Element of the carrier of f
(x0 /. x1) + (- (x0 /. x1)) is Element of the carrier of f
||.((x0 /. x1) - (x0 /. x1)).|| is V11() real ext-real Element of REAL
(x0 | X) /. x1 is Element of the carrier of f
((x0 | X) /. x1) - (x0 /. x1) is Element of the carrier of f
((x0 | X) /. x1) + (- (x0 /. x1)) is Element of the carrier of f
||.(((x0 | X) /. x1) - (x0 /. x1)).|| is V11() real ext-real Element of REAL
(x0 | X) /. x1 is Element of the carrier of f
((x0 | X) /. x1) - ((x0 | X) /. x1) is Element of the carrier of f
- ((x0 | X) /. x1) is Element of the carrier of f
((x0 | X) /. x1) + (- ((x0 | X) /. x1)) is Element of the carrier of f
||.(((x0 | X) /. x1) - ((x0 | X) /. x1)).|| is V11() real ext-real Element of REAL
p " is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
x2 * (p ") is V11() real ext-real Element of REAL
x1 is Element of the carrier of S
x1 - x1 is Element of the carrier of S
x1 + (- x1) is Element of the carrier of S
||.(x1 - x1).|| is V11() real ext-real Element of REAL
(x0 | X) /. x1 is Element of the carrier of f
((x0 | X) /. x1) - ((x0 | X) /. x1) is Element of the carrier of f
((x0 | X) /. x1) + (- ((x0 | X) /. x1)) is Element of the carrier of f
||.(((x0 | X) /. x1) - ((x0 | X) /. x1)).|| is V11() real ext-real Element of REAL
X is set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S,REAL) is set
K6(K7( the carrier of S,REAL)) is set
f is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
x0 is V11() real ext-real Element of REAL
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
f | X is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
dom (f | X) is Element of K6( the carrier of S)
p is Element of the carrier of S
x1 is V11() real ext-real Element of REAL
x1 / x0 is V11() real ext-real Element of REAL
x1 is Element of the carrier of S
x1 - p is Element of the carrier of S
- p is Element of the carrier of S
x1 + (- p) is Element of the carrier of S
||.(x1 - p).|| is V11() real ext-real Element of REAL
(x1 / x0) * x0 is V11() real ext-real Element of REAL
x0 * ||.(x1 - p).|| is V11() real ext-real Element of REAL
f /. x1 is V11() real ext-real Element of REAL
f /. p is V11() real ext-real Element of REAL
(f /. x1) - (f /. p) is V11() real ext-real Element of REAL
abs ((f /. x1) - (f /. p)) is V11() real ext-real Element of REAL
(f | X) /. x1 is V11() real ext-real Element of REAL
((f | X) /. x1) - (f /. p) is V11() real ext-real Element of REAL
abs (((f | X) /. x1) - (f /. p)) is V11() real ext-real Element of REAL
(f | X) /. p is V11() real ext-real Element of REAL
((f | X) /. x1) - ((f | X) /. p) is V11() real ext-real Element of REAL
abs (((f | X) /. x1) - ((f | X) /. p)) is V11() real ext-real Element of REAL
x0 " is V11() real ext-real Element of REAL
s9 is V11() real ext-real Element of REAL
x1 * (x0 ") is V11() real ext-real Element of REAL
x1 is Element of the carrier of S
x1 - p is Element of the carrier of S
x1 + (- p) is Element of the carrier of S
||.(x1 - p).|| is V11() real ext-real Element of REAL
(f | X) /. x1 is V11() real ext-real Element of REAL
((f | X) /. x1) - ((f | X) /. p) is V11() real ext-real Element of REAL
abs (((f | X) /. x1) - ((f | X) /. p)) is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of X) is set
K6(K7( the carrier of S, the carrier of X)) is set
f is Relation-like the carrier of S -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of S, the carrier of X))
rng f is Element of K6( the carrier of X)
K6( the carrier of X) is set
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
x0 is Element of the carrier of X
{x0} is non empty set
p is Element of the carrier of S
x1 is Element of the carrier of S
f . x1 is set
f /. x1 is Element of the carrier of X
f . p is set
f /. p is Element of the carrier of X
(f /. p) - (f /. x1) is Element of the carrier of X
- (f /. x1) is Element of the carrier of X
(f /. p) + (- (f /. x1)) is Element of the carrier of X
||.((f /. p) - (f /. x1)).|| is V11() real ext-real Element of REAL
0. X is V91(X) Element of the carrier of X
||.(0. X).|| is V11() real ext-real Element of REAL
p - x1 is Element of the carrier of S
- x1 is Element of the carrier of S
p + (- x1) is Element of the carrier of S
||.(p - x1).|| is V11() real ext-real Element of REAL
1 * ||.(p - x1).|| is V11() real ext-real Element of REAL
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
f is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of f is non empty set
K7( the carrier of S, the carrier of f) is set
K6(K7( the carrier of S, the carrier of f)) is set
X is set
x0 is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
dom x0 is Element of K6( the carrier of S)
K6( the carrier of S) is set
x0 | X is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of K6(K7( the carrier of S, the carrier of f))
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K7( the carrier of X, the carrier of X) is set
K6(K7( the carrier of X, the carrier of X)) is set
S is Relation-like the carrier of X -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of X, the carrier of X))
dom S is Element of K6( the carrier of X)
K6( the carrier of X) is set
f is Element of the carrier of X
x0 is Element of the carrier of X
S /. f is Element of the carrier of X
S /. x0 is Element of the carrier of X
(S /. f) - (S /. x0) is Element of the carrier of X
- (S /. x0) is Element of the carrier of X
(S /. f) + (- (S /. x0)) is Element of the carrier of X
||.((S /. f) - (S /. x0)).|| is V11() real ext-real Element of REAL
f - x0 is Element of the carrier of X
- x0 is Element of the carrier of X
f + (- x0) is Element of the carrier of X
||.(f - x0).|| is V11() real ext-real Element of REAL
1 * ||.(f - x0).|| is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K7( the carrier of X, the carrier of X) is set
K6(K7( the carrier of X, the carrier of X)) is set
S is Relation-like the carrier of X -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of X, the carrier of X))
dom S is Element of K6( the carrier of X)
K6( the carrier of X) is set
id (dom S) is Relation-like the carrier of X -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of X, the carrier of X))
f is Element of the carrier of X
S /. f is Element of the carrier of X
S . f is set
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K6( the carrier of X) is set
K7( the carrier of X, the carrier of X) is set
K6(K7( the carrier of X, the carrier of X)) is set
S is Element of K6( the carrier of X)
id S is Relation-like the carrier of X -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of X, the carrier of X))
f is Relation-like the carrier of X -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of X, the carrier of X))
dom f is Element of K6( the carrier of X)
f | S is Relation-like the carrier of X -defined the carrier of X -valued Function-like Element of K6(K7( the carrier of X, the carrier of X))
x0 is Element of the carrier of X
p is Element of the carrier of X
(dom f) /\ S is Element of K6( the carrier of X)
dom (f | S) is Element of K6( the carrier of X)
(f | S) . x0 is set
f . x0 is set
f /. x0 is Element of the carrier of X
(f | S) . p is set
f . p is set
f /. p is Element of the carrier of X
(f /. x0) - (f /. p) is Element of the carrier of X
- (f /. p) is Element of the carrier of X
(f /. x0) + (- (f /. p)) is Element of the carrier of X
||.((f /. x0) - (f /. p)).|| is V11() real ext-real Element of REAL
x0 - p is Element of the carrier of X
- p is Element of the carrier of X
x0 + (- p) is Element of the carrier of X
||.(x0 - p).|| is V11() real ext-real Element of REAL
1 * ||.(x0 - p).|| is V11() real ext-real Element of REAL
X is set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S, the carrier of S) is set
K6(K7( the carrier of S, the carrier of S)) is set
f is Relation-like the carrier of S -defined the carrier of S -valued Function-like Element of K6(K7( the carrier of S, the carrier of S))
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
x0 is V11() real ext-real Element of REAL
p is Element of the carrier of S
abs x0 is V11() real ext-real Element of REAL
(abs x0) + 1 is V11() real ext-real Element of REAL
0 + 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of REAL
x1 is Element of the carrier of S
x2 is Element of the carrier of S
f /. x1 is Element of the carrier of S
x0 * x1 is Element of the carrier of S
(x0 * x1) + p is Element of the carrier of S
f /. x2 is Element of the carrier of S
x0 * x2 is Element of the carrier of S
(x0 * x2) + p is Element of the carrier of S
(f /. x1) - (f /. x2) is Element of the carrier of S
- (f /. x2) is Element of the carrier of S
(f /. x1) + (- (f /. x2)) is Element of the carrier of S
||.((f /. x1) - (f /. x2)).|| is V11() real ext-real Element of REAL
p + (x0 * x2) is Element of the carrier of S
p - (p + (x0 * x2)) is Element of the carrier of S
- (p + (x0 * x2)) is Element of the carrier of S
p + (- (p + (x0 * x2))) is Element of the carrier of S
(x0 * x1) + (p - (p + (x0 * x2))) is Element of the carrier of S
||.((x0 * x1) + (p - (p + (x0 * x2)))).|| is V11() real ext-real Element of REAL
p - p is Element of the carrier of S
- p is Element of the carrier of S
p + (- p) is Element of the carrier of S
(p - p) - (x0 * x2) is Element of the carrier of S
- (x0 * x2) is Element of the carrier of S
(p - p) + (- (x0 * x2)) is Element of the carrier of S
(x0 * x1) + ((p - p) - (x0 * x2)) is Element of the carrier of S
||.((x0 * x1) + ((p - p) - (x0 * x2))).|| is V11() real ext-real Element of REAL
0. S is V91(S) Element of the carrier of S
(0. S) - (x0 * x2) is Element of the carrier of S
(0. S) + (- (x0 * x2)) is Element of the carrier of S
(x0 * x1) + ((0. S) - (x0 * x2)) is Element of the carrier of S
||.((x0 * x1) + ((0. S) - (x0 * x2))).|| is V11() real ext-real Element of REAL
(x0 * x1) - (x0 * x2) is Element of the carrier of S
(x0 * x1) + (- (x0 * x2)) is Element of the carrier of S
||.((x0 * x1) - (x0 * x2)).|| is V11() real ext-real Element of REAL
x1 - x2 is Element of the carrier of S
- x2 is Element of the carrier of S
x1 + (- x2) is Element of the carrier of S
x0 * (x1 - x2) is Element of the carrier of S
||.(x0 * (x1 - x2)).|| is V11() real ext-real Element of REAL
||.(x1 - x2).|| is V11() real ext-real Element of REAL
(abs x0) * ||.(x1 - x2).|| is V11() real ext-real Element of REAL
||.((f /. x1) - (f /. x2)).|| + 0 is V11() real ext-real Element of REAL
1 * ||.(x1 - x2).|| is V11() real ext-real Element of REAL
((abs x0) * ||.(x1 - x2).||) + (1 * ||.(x1 - x2).||) is V11() real ext-real Element of REAL
((abs x0) + 1) * ||.(x1 - x2).|| is V11() real ext-real Element of REAL
X is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of X is non empty set
K7( the carrier of X,REAL) is set
K6(K7( the carrier of X,REAL)) is set
S is Relation-like the carrier of X -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of X,REAL))
dom S is Element of K6( the carrier of X)
K6( the carrier of X) is set
f is Element of the carrier of X
x0 is Element of the carrier of X
S /. f is V11() real ext-real Element of REAL
||.f.|| is V11() real ext-real Element of REAL
S /. x0 is V11() real ext-real Element of REAL
||.x0.|| is V11() real ext-real Element of REAL
(S /. f) - (S /. x0) is V11() real ext-real Element of REAL
abs ((S /. f) - (S /. x0)) is V11() real ext-real Element of REAL
f - x0 is Element of the carrier of X
- x0 is Element of the carrier of X
f + (- x0) is Element of the carrier of X
||.(f - x0).|| is V11() real ext-real Element of REAL
1 * ||.(f - x0).|| is V11() real ext-real Element of REAL
X is set
S is non empty left_complementable right_complementable V135() V136() V137() V138() V139() V140() V141() zeroed V145() V146() RealNormSpace-like NORMSTR
the carrier of S is non empty set
K7( the carrier of S,REAL) is set
K6(K7( the carrier of S,REAL)) is set
f is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
dom f is Element of K6( the carrier of S)
K6( the carrier of S) is set
(dom f) /\ X is Element of K6( the carrier of S)
f | X is Relation-like the carrier of S -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of S,REAL))
dom (f | X) is Element of K6( the carrier of S)
x0 is Element of the carrier of S
(f | X) /. x0 is V11() real ext-real Element of REAL
f /. x0 is V11() real ext-real Element of REAL
||.x0.|| is V11() real ext-real Element of REAL