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

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

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

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

x2 is V11() real ext-real Element of REAL

{ b

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

x1 is (X,f /. x0)

x2 is (S,x0)

s9 is V11() real ext-real Element of REAL

{ b

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

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