:: NFCONT_1 semantic presentation

REAL is non empty V54() set

K6(REAL) is set
COMPLEX is non empty V54() set
RAT is non empty V54() set
INT is non empty V54() 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

- 1 is V11() real ext-real non positive Element of REAL
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))

(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

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

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

the carrier of X is non empty set
K6( the carrier of X) is set
S is Element of the carrier of X
{ b1 where b1 is Element of the carrier of X : not 1 <= ||.(b1 - 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

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
{ b1 where b1 is Element of the carrier of X : not f <= ||.(b1 - 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

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
{ b1 where b1 is Element of the carrier of X : not x0 <= ||.(b1 - 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

the carrier of X is non empty set
K6( the carrier of X) is set

the carrier of X is non empty set
K6( the carrier of X) is set

the carrier of X is non empty set
K6( the carrier of X) is set

the carrier of X is non empty set

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

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

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

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)

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

S . p is Element of the carrier of X

S . x0 is Element of the carrier of X
dom S is Element of K6(NAT)

the carrier of X is non empty set

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

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

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

(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

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

(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

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

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

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

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

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) . 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

(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

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

(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

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) . 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

the carrier of X is non empty set

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
{ b1 where b1 is Element of the carrier of X : not x1 <= ||.(b1 - (f /. x0)).|| } is set
x2 is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of S : not x2 <= ||.(b1 - 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
{ b1 where b1 is Element of the carrier of X : not p <= ||.(b1 - (f /. x0)).|| } is set
x1 is (X,f /. x0)
x2 is (S,x0)
s9 is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of S : not s9 <= ||.(b1 - 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
{ b1 where b1 is Element of the carrier of S : not x1 <= ||.(b1 - 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

the carrier of X is non empty set

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

the carrier of X is non empty set

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

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

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)

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)

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

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

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)

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

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

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

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 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 is Element of K6( the carrier of X)

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
. (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) * (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))

the carrier of X is non empty set

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

the carrier of S is non empty set

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

the carrier of X is non empty set

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

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

/. x0 is V11() real ext-real Element of REAL
. 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 ( /* 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))

the carrier of X is non empty set

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

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

the carrier of X is non empty set

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)

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)

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

the carrier of S is non empty set

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

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

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

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

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

the carrier of S is non empty set

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

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

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

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)

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

the carrier of X is non empty set

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)

x1 . x2 is Element of the carrier of S
x2 is V11() real ext-real Element of REAL

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

the carrier of X is non empty set

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