:: NFCONT_3 semantic presentation

REAL is non empty V13() V14() V15() V19() V57() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() Element of bool REAL

bool REAL is set

COMPLEX is non empty V13() V19() V57() set

[:REAL,REAL:] is Relation-like complex-valued ext-real-valued real-valued set

bool [:REAL,REAL:] is set

omega is non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() set

bool omega is set

bool NAT is set

[:NAT,REAL:] is Relation-like complex-valued ext-real-valued real-valued set

bool [:NAT,REAL:] is set

RAT is non empty V13() V14() V15() V16() V19() V57() set

INT is non empty V13() V14() V15() V16() V17() V19() V57() set

{} is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() V14() V15() V16() V17() V18() V19() ext-real non positive non negative Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real positive non negative Element of NAT

0 is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() V14() V15() V16() V17() V18() V19() ext-real non positive non negative Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of NAT

- 1 is V11() real ext-real non positive Element of REAL

X is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

S is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of S is non empty set

[:REAL, the carrier of S:] is Relation-like set

bool [:REAL, the carrier of S:] is set

f is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

rng f is non empty V13() V14() V15() Element of bool REAL

f . X is V11() real ext-real Element of REAL

r is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]

dom r is V13() V14() V15() Element of bool REAL

dom f is non empty V13() V14() V15() V16() V17() V18() Element of bool NAT

f (#) r is Relation-like NAT -defined the carrier of S -valued Function-like set

dom (f (#) r) is V13() V14() V15() V16() V17() V18() Element of bool NAT

X is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:REAL, the carrier of X:] is Relation-like set

bool [:REAL, the carrier of X:] is set

S is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

dom S is V13() V14() V15() Element of bool REAL

f is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

dom f is V13() V14() V15() Element of bool REAL

(dom S) /\ (dom f) is V13() V14() V15() Element of bool REAL

S + f is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

S - f is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

r is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

rng r is non empty V13() V14() V15() Element of bool REAL

(S + f) /* r is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

[:NAT, the carrier of X:] is Relation-like set

bool [:NAT, the carrier of X:] is set

S /* r is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

f /* r is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

(S /* r) + (f /* r) is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

(S - f) /* r is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

(S /* r) - (f /* r) is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

r . p is V11() real ext-real Element of REAL

S /. (r . p) is Element of the carrier of X

(S /* r) . p is Element of the carrier of X

f /. (r . p) is Element of the carrier of X

(f /* r) . p is Element of the carrier of X

dom (S + f) is V13() V14() V15() Element of bool REAL

((S + f) /* r) . p is Element of the carrier of X

(S + f) /. (r . p) is Element of the carrier of X

((S /* r) . p) + ((f /* r) . p) is Element of the carrier of X

p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

r . p is V11() real ext-real Element of REAL

S /. (r . p) is Element of the carrier of X

(S /* r) . p is Element of the carrier of X

f /. (r . p) is Element of the carrier of X

(f /* r) . p is Element of the carrier of X

dom (S - f) is V13() V14() V15() Element of bool REAL

((S - f) /* r) . p is Element of the carrier of X

(S - f) /. (r . p) is Element of the carrier of X

((S /* r) . p) - ((f /* r) . p) is Element of the carrier of X

- ((f /* r) . p) is Element of the carrier of X

K201(X,((S /* r) . p),(- ((f /* r) . p))) is Element of the carrier of X

X is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:NAT, the carrier of X:] is Relation-like set

bool [: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 bool [:NAT, the carrier of X:]

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

f (#) S is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

f * S is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

dom S is non empty V13() V14() V15() V16() V17() V18() Element of bool NAT

dom (f (#) S) is non empty V13() V14() V15() V16() V17() V18() Element of bool NAT

r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

(f (#) S) . r is Element of the carrier of X

(f (#) S) /. r is Element of the carrier of X

(f (#) S) . r is Element of the carrier of X

S /. r is Element of the carrier of X

S . r is Element of the carrier of X

f * (S /. r) is Element of the carrier of X

S . r is Element of the carrier of X

f * (S . r) is Element of the carrier of X

X is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:REAL, the carrier of X:] is Relation-like set

bool [:REAL, the carrier of X:] is set

S is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

dom S is V13() V14() V15() Element of bool REAL

f is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

rng f is non empty V13() V14() V15() Element of bool REAL

S /* f is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

[:NAT, the carrier of X:] is Relation-like set

bool [:NAT, the carrier of X:] is set

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

r (#) S is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

(r (#) S) /* f is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

r * (S /* f) is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

dom (r (#) S) is V13() V14() V15() Element of bool REAL

p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

f . p is V11() real ext-real Element of REAL

((r (#) S) /* f) . p is Element of the carrier of X

(r (#) S) /. (f . p) is Element of the carrier of X

S /. (f . p) is Element of the carrier of X

r * (S /. (f . p)) is Element of the carrier of X

(S /* f) . p is Element of the carrier of X

r * ((S /* f) . p) is Element of the carrier of X

X is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:REAL, the carrier of X:] is Relation-like set

bool [:REAL, the carrier of X:] is set

S is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

dom S is V13() V14() V15() Element of bool REAL

||.S.|| is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- S is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

f is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

rng f is non empty V13() V14() V15() Element of bool REAL

S /* f is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

[:NAT, the carrier of X:] is Relation-like set

bool [:NAT, the carrier of X:] is set

||.(S /* f).|| is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

||.S.|| /* f is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

- (S /* f) is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [: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 bool [:NAT, the carrier of X:]

dom ||.S.|| is V13() V14() V15() Element of bool REAL

r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

f . r is V11() real ext-real Element of REAL

||.(S /* f).|| . r is V11() real ext-real Element of REAL

(S /* f) . r is Element of the carrier of X

||.((S /* f) . r).|| is V11() real ext-real Element of REAL

S /. (f . r) is Element of the carrier of X

||.(S /. (f . r)).|| is V11() real ext-real Element of REAL

||.S.|| . (f . r) is V11() real ext-real Element of REAL

||.S.|| /. (f . r) is V11() real ext-real Element of REAL

(||.S.|| /* f) . r is V11() real ext-real Element of REAL

r is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

(- (S /* f)) . r is Element of the carrier of X

(S /* f) . r is Element of the carrier of X

- ((S /* f) . r) is Element of the carrier of X

(- 1) * ((S /* f) . r) is Element of the carrier of X

(- 1) * (S /* f) is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

((- 1) * (S /* f)) . r is Element of the carrier of X

(- 1) (#) S is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

((- 1) (#) S) /* f is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

(((- 1) (#) S) /* f) . r is Element of the carrier of X

((- S) /* f) . r is Element of the carrier of X

X is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:REAL, the carrier of X:] is Relation-like set

bool [:REAL, the carrier of X:] is set

X is set

S is V11() real ext-real set

f is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of f is non empty set

[:REAL, the carrier of f:] is Relation-like set

bool [:REAL, the carrier of f:] is set

r is Relation-like REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]

r | X is Relation-like REAL -defined X -defined REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]

dom r is V13() V14() V15() Element of bool REAL

dom (r | X) is Element of bool X

bool X is set

X /\ (dom r) is V13() V14() V15() Element of bool REAL

dom (r | X) is V13() V14() V15() Element of bool REAL

(r | X) /. S is Element of the carrier of 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 bool [:NAT,REAL:]

rng p is non empty V13() V14() V15() Element of bool REAL

lim p is V11() real ext-real Element of REAL

(r | X) /* p is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total Element of bool [:NAT, the carrier of f:]

[:NAT, the carrier of f:] is Relation-like set

bool [:NAT, the carrier of f:] is set

lim ((r | X) /* p) is Element of the carrier of f

r /* p is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total Element of bool [:NAT, the carrier of f:]

r /. S is Element of the carrier of f

X is V11() real ext-real set

S is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of S is non empty set

[:REAL, the carrier of S:] is Relation-like set

bool [:REAL, the carrier of S:] is set

f is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]

dom f is V13() V14() V15() Element of bool REAL

f /. X is Element of the carrier of S

r is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

rng r is non empty V13() V14() V15() Element of bool REAL

lim r is V11() real ext-real Element of REAL

f /* r is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

[:NAT, the carrier of S:] is Relation-like set

bool [:NAT, the carrier of S:] is set

lim (f /* r) is Element of the carrier of S

r is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

rng r is non empty V13() V14() V15() Element of bool REAL

lim r is V11() real ext-real Element of REAL

f /* r is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

[:NAT, the carrier of S:] is Relation-like set

bool [:NAT, the carrier of S:] is set

lim (f /* r) is Element of the carrier of S

p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

r ^\ p is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of r

f /* (r ^\ p) is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

(f /* r) ^\ p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total subsequence of f /* r

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

x2 is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() V14() V15() V16() V17() V18() V19() ext-real non positive non negative Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of NAT

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

s9 + p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

r . (s9 + p) is V11() real ext-real Element of REAL

rng (r ^\ p) is non empty V13() V14() V15() Element of bool REAL

(f /* (r ^\ p)) . s9 is Element of the carrier of S

((f /* (r ^\ p)) . s9) - (f /. X) is Element of the carrier of S

- (f /. X) is Element of the carrier of S

K201(S,((f /* (r ^\ p)) . s9),(- (f /. X))) is Element of the carrier of S

||.(((f /* (r ^\ p)) . s9) - (f /. X)).|| is V11() real ext-real Element of REAL

(r ^\ p) . s9 is V11() real ext-real Element of REAL

f /. ((r ^\ p) . s9) is Element of the carrier of S

(f /. ((r ^\ p) . s9)) - (f /. X) is Element of the carrier of S

K201(S,(f /. ((r ^\ p) . s9)),(- (f /. X))) is Element of the carrier of S

||.((f /. ((r ^\ p) . s9)) - (f /. X)).|| is V11() real ext-real Element of REAL

(f /. X) - (f /. X) is Element of the carrier of S

K201(S,(f /. X),(- (f /. X))) is Element of the carrier of S

||.((f /. X) - (f /. X)).|| is V11() real ext-real Element of REAL

lim ((f /* r) ^\ p) is Element of the carrier of S

p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

r . p is V11() real ext-real Element of REAL

p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

r . p is V11() real ext-real Element of REAL

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

x2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real positive non negative Element of NAT

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

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

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

r . x1 is V11() real ext-real Element of REAL

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

r . x1 is V11() real ext-real Element of REAL

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

r . x1 is V11() real ext-real Element of REAL

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

r . n is V11() real ext-real Element of REAL

k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

r . k is V11() real ext-real Element of REAL

[:NAT,NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:NAT,NAT:] is set

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

x2 is non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]

x2 . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of REAL

dom x2 is non empty V13() V14() V15() V16() V17() V18() Element of bool NAT

rng x2 is non empty V13() V14() V15() V16() V17() V18() Element of bool NAT

s9 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

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

rng s9 is non empty V13() V14() V15() Element of bool REAL

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

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

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real positive non negative Element of NAT

s9 . (x1 + 1) is V11() real ext-real Element of REAL

x1 is non empty Relation-like NAT -defined NAT -valued Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

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

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

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

n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

x1 . 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of REAL

k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

r . k is V11() real ext-real Element of REAL

k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

x1 . k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of REAL

k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set

r . k is V11() real ext-real Element of REAL

k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

x1 . k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of REAL

k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

x1 . k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of REAL

k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real positive non negative Element of NAT

x1 . (k + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of REAL

r . (x1 . (k + 1)) is V11() real ext-real Element of REAL

m is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

x1 . m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of REAL

m is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

x1 . m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of REAL

r * x1 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued subsequence of r

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

(r * x1) . x2 is V11() real ext-real Element of REAL

x2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real positive non negative Element of NAT

(r * x1) . (x2 + 1) is V11() real ext-real Element of REAL

x1 . x2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of REAL

x1 . (x2 + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of REAL

r . (x1 . (x2 + 1)) is V11() real ext-real Element of REAL

(r * x1) . 0 is V11() real ext-real Element of REAL

lim (r * x1) is V11() real ext-real Element of REAL

rng (r * x1) is non empty V13() V14() V15() Element of bool REAL

f /* (r * x1) is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

lim (f /* (r * x1)) is Element of the carrier of S

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

n is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

x1 . n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of REAL

k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

r . m is V11() real ext-real Element of REAL

(f /* r) . m is Element of the carrier of S

((f /* r) . m) - (f /. X) is Element of the carrier of S

- (f /. X) is Element of the carrier of S

K201(S,((f /* r) . m),(- (f /. X))) is Element of the carrier of S

||.(((f /* r) . m) - (f /. X)).|| is V11() real ext-real Element of REAL

(f /. X) - (f /. X) is Element of the carrier of S

K201(S,(f /. X),(- (f /. X))) is Element of the carrier of S

||.((f /. X) - (f /. X)).|| is V11() real ext-real Element of REAL

r . m is V11() real ext-real Element of REAL

l is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

x1 . l is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of REAL

(f /* (r * x1)) . l is Element of the carrier of S

((f /* (r * x1)) . l) - (f /. X) is Element of the carrier of S

- (f /. X) is Element of the carrier of S

K201(S,((f /* (r * x1)) . l),(- (f /. X))) is Element of the carrier of S

||.(((f /* (r * x1)) . l) - (f /. X)).|| is V11() real ext-real Element of REAL

(r * x1) . l is V11() real ext-real Element of REAL

f /. ((r * x1) . l) is Element of the carrier of S

(f /. ((r * x1) . l)) - (f /. X) is Element of the carrier of S

K201(S,(f /. ((r * x1) . l)),(- (f /. X))) is Element of the carrier of S

||.((f /. ((r * x1) . l)) - (f /. X)).|| is V11() real ext-real Element of REAL

f /. (r . m) is Element of the carrier of S

(f /. (r . m)) - (f /. X) is Element of the carrier of S

K201(S,(f /. (r . m)),(- (f /. X))) is Element of the carrier of S

||.((f /. (r . m)) - (f /. X)).|| is V11() real ext-real Element of REAL

(f /* r) . m is Element of the carrier of S

((f /* r) . m) - (f /. X) is Element of the carrier of S

K201(S,((f /* r) . m),(- (f /. X))) is Element of the carrier of S

||.(((f /* r) . m) - (f /. X)).|| is V11() real ext-real Element of REAL

r . m is V11() real ext-real Element of REAL

p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

X is V11() real ext-real set

S is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of S is non empty set

[:REAL, the carrier of S:] is Relation-like set

bool [:REAL, the carrier of S:] is set

f is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]

dom f is V13() V14() V15() Element of bool REAL

f /. X is Element of the carrier of S

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

p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real positive non negative Element of NAT

1 / (p + 1) is V11() real ext-real non negative Element of COMPLEX

(p + 1) " is non empty V11() real ext-real positive non negative Element of REAL

x1 is V11() real ext-real set

x1 - X is V11() real ext-real set

abs (x1 - X) is V11() real ext-real Element of REAL

f /. x1 is Element of the carrier of S

(f /. x1) - (f /. X) is Element of the carrier of S

- (f /. X) is Element of the carrier of S

K201(S,(f /. x1),(- (f /. X))) is Element of the carrier of S

||.((f /. x1) - (f /. X)).|| is V11() real ext-real Element of REAL

p is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

x1 is set

rng p is non empty V13() V14() V15() Element of bool REAL

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

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

x1 is V11() real ext-real set

x1 " is V11() real ext-real set

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

x2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real positive non negative Element of NAT

(x1 ") + 0 is V11() real ext-real set

1 / (x1 ") is V11() real ext-real Element of COMPLEX

1 / (x2 + 1) is V11() real ext-real non negative Element of COMPLEX

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

s9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real positive non negative Element of NAT

x1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real positive non negative Element of NAT

1 / (x1 + 1) is V11() real ext-real non negative Element of COMPLEX

1 / (s9 + 1) is V11() real ext-real non negative Element of COMPLEX

p . x1 is V11() real ext-real Element of REAL

(p . x1) - X is V11() real ext-real Element of REAL

abs ((p . x1) - X) is V11() real ext-real Element of REAL

lim p is V11() real ext-real Element of REAL

f /* p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

[:NAT, the carrier of S:] is Relation-like set

bool [:NAT, the carrier of S:] is set

lim (f /* p) is Element of the carrier of S

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

(f /* p) . x1 is Element of the carrier of S

((f /* p) . x1) - (f /. X) is Element of the carrier of S

- (f /. X) is Element of the carrier of S

K201(S,((f /* p) . x1),(- (f /. X))) is Element of the carrier of S

||.(((f /* p) . x1) - (f /. X)).|| is V11() real ext-real Element of REAL

p . x1 is V11() real ext-real Element of REAL

f /. (p . x1) is Element of the carrier of S

(f /. (p . x1)) - (f /. X) is Element of the carrier of S

K201(S,(f /. (p . x1)),(- (f /. X))) is Element of the carrier of S

||.((f /. (p . x1)) - (f /. X)).|| is V11() real ext-real Element of REAL

r is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

rng r is non empty V13() V14() V15() Element of bool REAL

lim r is V11() real ext-real Element of REAL

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

x1 is V11() real ext-real set

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

r . x1 is V11() real ext-real Element of REAL

(r . x1) - X is V11() real ext-real Element of REAL

abs ((r . x1) - X) is V11() real ext-real Element of REAL

f /. (r . x1) is Element of the carrier of S

(f /. (r . x1)) - (f /. X) is Element of the carrier of S

- (f /. X) is Element of the carrier of S

K201(S,(f /. (r . x1)),(- (f /. X))) is Element of the carrier of S

||.((f /. (r . x1)) - (f /. X)).|| is V11() real ext-real Element of REAL

f /* r is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

[:NAT, the carrier of S:] is Relation-like set

bool [:NAT, the carrier of S:] is set

(f /* r) . x1 is Element of the carrier of S

((f /* r) . x1) - (f /. X) is Element of the carrier of S

K201(S,((f /* r) . x1),(- (f /. X))) is Element of the carrier of S

||.(((f /* r) . x1) - (f /. X)).|| is V11() real ext-real Element of REAL

lim (f /* r) is Element of the carrier of S

X is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:REAL, the carrier of X:] is Relation-like set

bool [:REAL, the carrier of X:] is set

S is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

dom S is V13() V14() V15() Element of bool REAL

f is V11() real ext-real set

S /. f is Element of the carrier of X

r is Neighbourhood of S /. f

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

{ b

x2 is V11() real ext-real set

f - x2 is V11() real ext-real set

f + x2 is V11() real ext-real set

].(f - x2),(f + x2).[ is V13() V14() V15() Element of bool REAL

s9 is V13() V14() V15() Neighbourhood of f

x1 is V11() real ext-real set

S /. x1 is Element of the carrier of X

x1 - f is V11() real ext-real set

abs (x1 - f) is V11() real ext-real Element of REAL

(S /. x1) - (S /. f) is Element of the carrier of X

- (S /. f) is Element of the carrier of X

K201(X,(S /. x1),(- (S /. f))) is Element of the carrier of X

||.((S /. x1) - (S /. f)).|| is V11() real ext-real Element of REAL

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

{ b

p is Neighbourhood of S /. f

x1 is V13() V14() V15() Neighbourhood of f

x2 is V11() real ext-real set

f - x2 is V11() real ext-real set

f + x2 is V11() real ext-real set

].(f - x2),(f + x2).[ is V13() V14() V15() Element of bool REAL

s9 is V11() real ext-real set

x1 is V11() real ext-real set

x1 - f is V11() real ext-real set

abs (x1 - f) is V11() real ext-real Element of REAL

S /. x1 is Element of the carrier of X

(S /. x1) - (S /. f) is Element of the carrier of X

- (S /. f) is Element of the carrier of X

K201(X,(S /. x1),(- (S /. f))) is Element of the carrier of X

||.((S /. x1) - (S /. f)).|| is V11() real ext-real Element of REAL

x2 is Element of the carrier of X

x2 - (S /. f) is Element of the carrier of X

K201(X,x2,(- (S /. f))) is Element of the carrier of X

||.(x2 - (S /. f)).|| is V11() real ext-real Element of REAL

x1 is V11() real ext-real set

x1 - f is V11() real ext-real set

abs (x1 - f) is V11() real ext-real Element of REAL

S /. x1 is Element of the carrier of X

(S /. x1) - (S /. f) is Element of the carrier of X

- (S /. f) is Element of the carrier of X

K201(X,(S /. x1),(- (S /. f))) is Element of the carrier of X

||.((S /. x1) - (S /. f)).|| is V11() real ext-real Element of REAL

X is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:REAL, the carrier of X:] is Relation-like set

bool [:REAL, the carrier of X:] is set

S is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

dom S is V13() V14() V15() Element of bool REAL

f is V11() real ext-real set

S /. f is Element of the carrier of X

r is Neighbourhood of S /. f

p is V13() V14() V15() Neighbourhood of f

S .: p is Element of bool the carrier of X

bool the carrier of X is set

x1 is set

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

S . x2 is set

S /. x2 is Element of the carrier of X

r is Neighbourhood of S /. f

p is V13() V14() V15() Neighbourhood of f

S .: p is Element of bool the carrier of X

bool the carrier of X is set

x2 is V11() real ext-real set

x1 is V13() V14() V15() Neighbourhood of f

S . x2 is set

S .: x1 is Element of bool the carrier of X

S /. x2 is Element of the carrier of X

X is V11() real ext-real set

{X} is non empty trivial V13() V14() V15() set

S is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of S is non empty set

[:REAL, the carrier of S:] is Relation-like set

bool [:REAL, the carrier of S:] is set

f is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]

dom f is V13() V14() V15() Element of bool REAL

r is V13() V14() V15() Neighbourhood of X

(dom f) /\ r is V13() V14() V15() Element of bool REAL

f /. X is Element of the carrier of S

p is Neighbourhood of f /. X

x1 is V13() V14() V15() Neighbourhood of X

f .: x1 is Element of bool the carrier of S

bool the carrier of S is set

Im (f,X) is set

f .: {X} is set

f . X is set

{(f . X)} is non empty trivial set

{(f /. X)} is non empty trivial set

X is V11() real ext-real set

S is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of S is non empty set

[:REAL, the carrier of S:] is Relation-like set

bool [:REAL, the carrier of S:] is set

f is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]

dom f is V13() V14() V15() Element of bool REAL

r is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]

dom r is V13() V14() V15() Element of bool REAL

(dom f) /\ (dom r) is V13() V14() V15() Element of bool REAL

f + r is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]

f - r is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]

dom (f + r) is V13() V14() V15() Element of bool REAL

p is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

rng p is non empty V13() V14() V15() Element of bool REAL

lim p is V11() real ext-real Element of REAL

f /* p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

[:NAT, the carrier of S:] is Relation-like set

bool [:NAT, the carrier of S:] is set

r /* p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

(f /* p) + (r /* p) is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

(f + r) /* p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

f /. X is Element of the carrier of S

lim (f /* p) is Element of the carrier of S

r /. X is Element of the carrier of S

lim (r /* p) is Element of the carrier of S

(f + r) /. X is Element of the carrier of S

(f /. X) + (r /. X) is Element of the carrier of S

lim ((f /* p) + (r /* p)) is Element of the carrier of S

lim ((f + r) /* p) is Element of the carrier of S

dom (f - r) is V13() V14() V15() Element of bool REAL

p is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

rng p is non empty V13() V14() V15() Element of bool REAL

lim p is V11() real ext-real Element of REAL

f /* p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

r /* p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

(f /* p) - (r /* p) is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

(f - r) /* p is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

lim (f /* p) is Element of the carrier of S

lim (r /* p) is Element of the carrier of S

(f - r) /. X is Element of the carrier of S

(f /. X) - (r /. X) is Element of the carrier of S

- (r /. X) is Element of the carrier of S

K201(S,(f /. X),(- (r /. X))) is Element of the carrier of S

lim ((f /* p) - (r /* p)) is Element of the carrier of S

lim ((f - r) /* p) is Element of the carrier of S

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

S is V11() real ext-real set

f is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of f is non empty set

[:REAL, the carrier of f:] is Relation-like set

bool [:REAL, the carrier of f:] is set

r is Relation-like REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]

X (#) r is Relation-like REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]

dom r is V13() V14() V15() Element of bool REAL

dom (X (#) r) is V13() V14() V15() Element of bool REAL

(X (#) r) /. S is Element of the carrier of 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 bool [:NAT,REAL:]

rng p is non empty V13() V14() V15() Element of bool REAL

lim p is V11() real ext-real Element of REAL

(X (#) r) /* p is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total Element of bool [:NAT, the carrier of f:]

[:NAT, the carrier of f:] is Relation-like set

bool [:NAT, the carrier of f:] is set

lim ((X (#) r) /* p) is Element of the carrier of f

r /. S is Element of the carrier of f

r /* p is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total Element of bool [:NAT, the carrier of f:]

lim (r /* p) is Element of the carrier of f

X * (r /* p) is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total Element of bool [:NAT, the carrier of f:]

X * (r /. S) is Element of the carrier of f

lim (X * (r /* p)) is Element of the carrier of f

X is V11() real ext-real set

S is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of S is non empty set

[:REAL, the carrier of S:] is Relation-like set

bool [:REAL, the carrier of S:] is set

f is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]

dom f is V13() V14() V15() Element of bool REAL

||.f.|| is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]

- f is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]

dom ||.f.|| is V13() V14() V15() Element of bool REAL

r is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

rng r is non empty V13() V14() V15() Element of bool REAL

lim r is V11() real ext-real Element of REAL

f /. X is Element of the carrier of S

f /* r is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

[:NAT, the carrier of S:] is Relation-like set

bool [:NAT, the carrier of S:] is set

lim (f /* r) is Element of the carrier of S

||.(f /* r).|| is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

||.f.|| /* r is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

||.f.|| . X is V11() real ext-real Element of REAL

||.(f /. X).|| is V11() real ext-real Element of REAL

lim ||.(f /* r).|| is V11() real ext-real Element of REAL

lim (||.f.|| /* r) is V11() real ext-real Element of REAL

(- 1) (#) f is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]

X is V11() real ext-real set

S is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of S is non empty set

[:REAL, the carrier of S:] is Relation-like set

bool [:REAL, the carrier of S:] is set

f is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of f is non empty set

[: the carrier of S, the carrier of f:] is Relation-like set

bool [: the carrier of S, the carrier of f:] is set

r is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]

r /. X is Element of the carrier of S

p is Relation-like the carrier of S -defined the carrier of f -valued Function-like Element of bool [: the carrier of S, the carrier of f:]

p * r is Relation-like REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]

[:REAL, the carrier of f:] is Relation-like set

bool [:REAL, the carrier of f:] is set

dom (p * r) is V13() V14() V15() Element of bool REAL

(p * r) /. X is Element of the carrier of 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 bool [:NAT,REAL:]

rng x1 is non empty V13() V14() V15() Element of bool REAL

lim x1 is V11() real ext-real Element of REAL

(p * r) /* x1 is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total Element of bool [:NAT, the carrier of f:]

[:NAT, the carrier of f:] is Relation-like set

bool [:NAT, the carrier of f:] is set

lim ((p * r) /* x1) is Element of the carrier of f

dom r is V13() V14() V15() Element of bool REAL

x2 is set

r /* x1 is non empty Relation-like NAT -defined the carrier of S -valued Function-like total quasi_total Element of bool [:NAT, the carrier of S:]

[:NAT, the carrier of S:] is Relation-like set

bool [:NAT, the carrier of S:] is set

rng (r /* x1) is non empty Element of bool the carrier of S

bool the carrier of S is set

s9 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

(r /* x1) . s9 is Element of the carrier of S

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

r . (x1 . s9) is set

dom p is Element of bool the carrier of S

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

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

((p * r) /* x1) . x2 is Element of the carrier of f

(p * r) . (x1 . x2) is set

r . (x1 . x2) is set

p . (r . (x1 . x2)) is set

(r /* x1) . x2 is Element of the carrier of S

p . ((r /* x1) . x2) is set

p /* (r /* x1) is non empty Relation-like NAT -defined the carrier of f -valued Function-like total quasi_total Element of bool [:NAT, the carrier of f:]

(p /* (r /* x1)) . x2 is Element of the carrier of f

lim (r /* x1) is Element of the carrier of S

p /. (r /. X) is Element of the carrier of f

lim (p /* (r /* x1)) is Element of the carrier of f

X is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:REAL, the carrier of X:] is Relation-like set

bool [:REAL, the carrier of X:] is set

X is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:REAL, the carrier of X:] is Relation-like set

bool [:REAL, the carrier of X:] is set

S is set

f is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

dom f is V13() V14() V15() Element of bool REAL

f | S is Relation-like REAL -defined S -defined REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

r is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

rng r is non empty V13() V14() V15() Element of bool REAL

lim r is V11() real ext-real Element of REAL

dom (f | S) is Element of bool S

bool S is set

(dom f) /\ S is V13() V14() V15() Element of bool REAL

p is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

r . p is V11() real ext-real Element of REAL

(f | S) /* r is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

[:NAT, the carrier of X:] is Relation-like set

bool [:NAT, the carrier of X:] is set

((f | S) /* r) . p is Element of the carrier of X

(f | S) /. (r . p) is Element of the carrier of X

f /. (r . p) is Element of the carrier of X

f /* r is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

(f /* r) . p is Element of the carrier of X

f /. (lim r) is Element of the carrier of X

(f | S) /. (lim r) is Element of the carrier of X

lim (f /* r) is Element of the carrier of X

dom (f | S) is Element of bool S

bool S is set

(dom f) /\ S is V13() V14() V15() Element of bool REAL

r is V11() real ext-real set

p is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

rng p is non empty V13() V14() V15() Element of bool REAL

lim p is V11() real ext-real Element of REAL

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

p . x1 is V11() real ext-real Element of REAL

(f | S) /* p is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

[:NAT, the carrier of X:] is Relation-like set

bool [:NAT, the carrier of X:] is set

((f | S) /* p) . x1 is Element of the carrier of X

(f | S) /. (p . x1) is Element of the carrier of X

f /. (p . x1) 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 bool [:NAT, the carrier of X:]

(f /* p) . x1 is Element of the carrier of X

(f | S) /. (lim p) is Element of the carrier of X

f /. (lim p) is Element of the carrier of X

lim ((f | S) /* p) is Element of the carrier of X

(f | S) /. r is Element of the carrier of X

X is set

S is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of S is non empty set

[:REAL, the carrier of S:] is Relation-like set

bool [:REAL, the carrier of S:] is set

f is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]

dom f is V13() V14() V15() Element of bool REAL

f | X is Relation-like REAL -defined X -defined REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]

r is V11() real ext-real set

f /. r is Element of the carrier of S

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

dom (f | X) is Element of bool X

bool X is set

(f | X) /. r is Element of the carrier of S

x1 is V11() real ext-real set

x2 is V11() real ext-real set

x2 - r is V11() real ext-real set

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

f /. x2 is Element of the carrier of S

(f /. x2) - (f /. r) is Element of the carrier of S

- (f /. r) is Element of the carrier of S

K201(S,(f /. x2),(- (f /. r))) is Element of the carrier of S

||.((f /. x2) - (f /. r)).|| is V11() real ext-real Element of REAL

(dom f) /\ X is V13() V14() V15() Element of bool REAL

(f | X) /. x2 is Element of the carrier of S

((f | X) /. x2) - (f /. r) is Element of the carrier of S

K201(S,((f | X) /. x2),(- (f /. r))) is Element of the carrier of S

||.(((f | X) /. x2) - (f /. r)).|| is V11() real ext-real Element of REAL

((f | X) /. x2) - ((f | X) /. r) is Element of the carrier of S

- ((f | X) /. r) is Element of the carrier of S

K201(S,((f | X) /. x2),(- ((f | X) /. r))) is Element of the carrier of S

||.(((f | X) /. x2) - ((f | X) /. r)).|| is V11() real ext-real Element of REAL

r is V11() real ext-real set

dom (f | X) is Element of bool X

bool X is set

(f | X) /. r is Element of the carrier of S

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

f /. r is Element of the carrier of S

x1 is V11() real ext-real set

x2 is V11() real ext-real set

x2 - r is V11() real ext-real set

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

(f | X) /. x2 is Element of the carrier of S

((f | X) /. x2) - ((f | X) /. r) is Element of the carrier of S

- ((f | X) /. r) is Element of the carrier of S

K201(S,((f | X) /. x2),(- ((f | X) /. r))) is Element of the carrier of S

||.(((f | X) /. x2) - ((f | X) /. r)).|| is V11() real ext-real Element of REAL

((f | X) /. x2) - (f /. r) is Element of the carrier of S

- (f /. r) is Element of the carrier of S

K201(S,((f | X) /. x2),(- (f /. r))) is Element of the carrier of S

||.(((f | X) /. x2) - (f /. r)).|| is V11() real ext-real Element of REAL

f /. x2 is Element of the carrier of S

(f /. x2) - (f /. r) is Element of the carrier of S

K201(S,(f /. x2),(- (f /. r))) is Element of the carrier of S

||.((f /. x2) - (f /. r)).|| is V11() real ext-real Element of REAL

X is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:REAL, the carrier of X:] is Relation-like set

bool [:REAL, the carrier of X:] is set

S is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

r is V11() real ext-real set

dom S is V13() V14() V15() Element of bool REAL

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

f is V11() real ext-real set

x1 is V11() real ext-real set

x2 is V11() real ext-real set

x2 - r is V11() real ext-real set

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

S /. x2 is Element of the carrier of X

S . x2 is set

S . r is set

S /. r is Element of the carrier of X

(S /. x2) - (S /. r) is Element of the carrier of X

- (S /. r) is Element of the carrier of X

K201(X,(S /. x2),(- (S /. r))) is Element of the carrier of X

||.((S /. x2) - (S /. r)).|| is V11() real ext-real Element of REAL

S | (dom S) is Relation-like REAL -defined dom S -defined REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

X is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:REAL, the carrier of X:] is Relation-like set

bool [:REAL, the carrier of X:] is set

the Relation-like REAL -defined the carrier of X -valued Function-like constant (X) Element of bool [:REAL, the carrier of X:] is Relation-like REAL -defined the carrier of X -valued Function-like constant (X) Element of bool [:REAL, the carrier of X:]

X is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:REAL, the carrier of X:] is Relation-like set

bool [:REAL, the carrier of X:] is set

S is Relation-like REAL -defined the carrier of X -valued Function-like (X) Element of bool [:REAL, the carrier of X:]

f is set

S | f is Relation-like REAL -defined f -defined REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

r is V11() real ext-real set

dom (S | f) is Element of bool f

bool f is set

dom S is V13() V14() V15() Element of bool REAL

r is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

X is set

S is set

f is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of f is non empty set

[:REAL, the carrier of f:] is Relation-like set

bool [:REAL, the carrier of f:] is set

r is Relation-like REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]

r | X is Relation-like REAL -defined X -defined REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]

r | S is Relation-like REAL -defined S -defined REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]

(r | X) | S is Relation-like REAL -defined S -defined REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]

X is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:REAL, the carrier of X:] is Relation-like set

bool [:REAL, the carrier of X:] is set

S is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

X is non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like NORMSTR

the carrier of X is non empty set

[:REAL, the carrier of X:] is Relation-like set

bool [:REAL, the carrier of X:] is set

S is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

f is trivial set

S | f is Relation-like REAL -defined f -defined REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

dom (S | f) is V13() V14() V15() Element of bool REAL

r is V11() real ext-real set

{r} is non empty trivial V13() V14() V15() set

p is V11() real ext-real set

dom (S | f) is Element of bool f

bool f is set

(S | f) /. p is Element of the carrier of X

x1 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]

rng x1 is non empty V13() V14() V15() Element of bool REAL

lim x1 is V11() real ext-real Element of REAL

(S | f) /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]

[:NAT, the carrier of X:] is Relation-like set

bool [:NAT, the carrier of X:] is set

lim ((S | f) /* x1) is Element of the carrier of X

dom S is V13() V14() V15() Element of bool REAL

(dom S) /\ {r} is V13() V14() V15() Element of bool REAL

x2 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

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

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

s9 is empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() V14() V15() V16() V17() V18() V19() ext-real non positive non negative Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing Element of NAT

x1 is epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative Element of NAT

S | {r} is Relation-like REAL -defined {r} -defined REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]

(S | {r}) /* x1 is non empty Relation-like NAT -defined the carrier of X -valued Function-like total quasi_total Element of bool