:: 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₁ where b₁ is Element of the carrier of X : not p <= ||.(b₁ - (S /. f)).|| } is set
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₁ where b₁ is Element of the carrier of X : not r <= ||.(b₁ - (S /. f)).|| } is set
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 [:NAT, the carrier of X:]
((S | {r}) /* x1) . x1 is Element of the carrier of X
(S | {r}) /. p is Element of the carrier of X
(((S | {r}) /* x1) . x1) - ((S | {r}) /. p) is Element of the carrier of X
- ((S | {r}) /. p) is Element of the carrier of X
K201(X,(((S | {r}) /* x1) . x1),(- ((S | {r}) /. p))) is Element of the carrier of X
||.((((S | {r}) /* x1) . x1) - ((S | {r}) /. p)).|| is V11() real ext-real Element of REAL
x1 . x1 is V11() real ext-real Element of REAL
(S | {r}) /. (x1 . x1) is Element of the carrier of X
(S | {r}) /. r is Element of the carrier of X
((S | {r}) /. (x1 . x1)) - ((S | {r}) /. r) is Element of the carrier of X
- ((S | {r}) /. r) is Element of the carrier of X
K201(X,((S | {r}) /. (x1 . x1)),(- ((S | {r}) /. r))) is Element of the carrier of X
||.(((S | {r}) /. (x1 . x1)) - ((S | {r}) /. r)).|| is V11() real ext-real Element of REAL
((S | {r}) /. r) - ((S | {r}) /. r) is Element of the carrier of X
K201(X,((S | {r}) /. r),(- ((S | {r}) /. r))) is Element of the carrier of X
||.(((S | {r}) /. r) - ((S | {r}) /. r)).|| is V11() real ext-real Element of REAL
p is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
r 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 (X) Element of bool [:REAL, the carrier of X:]
f is Relation-like REAL -defined the carrier of X -valued Function-like (X) 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:]
dom (S + f) is V13() V14() V15() Element of bool REAL
dom S is V13() V14() V15() Element of bool REAL
dom f is V13() V14() V15() Element of bool REAL
(dom S) /\ (dom f) is V13() V14() V15() Element of bool REAL
S | (dom (S + f)) is Relation-like REAL -defined dom (S + f) -defined REAL -defined the carrier of X -valued the carrier of X -valued Function-like (X) Element of bool [:REAL, the carrier of X:]
f | (dom (S + f)) is Relation-like REAL -defined dom (S + f) -defined REAL -defined the carrier of X -valued the carrier of X -valued Function-like (X) Element of bool [:REAL, the carrier of X:]
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
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 /* 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:]
(S /* p) + (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:]
S /. (lim p) is Element of the carrier of X
lim (S /* p) is Element of the carrier of X
f /. (lim p) is Element of the carrier of X
lim (f /* p) is Element of the carrier of X
(S + f) /. (lim p) is Element of the carrier of X
(lim (S /* p)) + (lim (f /* p)) is Element of the carrier of X
lim ((S /* p) + (f /* p)) is Element of the carrier of X
(S + 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:]
lim ((S + f) /* p) is Element of the carrier of X
(S + f) | (dom (S + f)) is Relation-like REAL -defined dom (S + f) -defined REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
p 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:]
dom (S - f) is V13() V14() V15() Element of bool REAL
dom S is V13() V14() V15() Element of bool REAL
dom f is V13() V14() V15() Element of bool REAL
(dom S) /\ (dom f) is V13() V14() V15() Element of bool REAL
S | (dom (S - f)) is Relation-like REAL -defined dom (S - f) -defined REAL -defined the carrier of X -valued the carrier of X -valued Function-like (X) Element of bool [:REAL, the carrier of X:]
f | (dom (S - f)) is Relation-like REAL -defined dom (S - f) -defined REAL -defined the carrier of X -valued the carrier of X -valued Function-like (X) Element of bool [:REAL, the carrier of X:]
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
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 /* 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:]
(S /* p) - (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:]
S /. (lim p) is Element of the carrier of X
lim (S /* p) is Element of the carrier of X
f /. (lim p) is Element of the carrier of X
lim (f /* p) is Element of the carrier of X
(S - f) /. (lim p) is Element of the carrier of X
(lim (S /* p)) - (lim (f /* p)) is Element of the carrier of X
- (lim (f /* p)) is Element of the carrier of X
K201(X,(lim (S /* p)),(- (lim (f /* p)))) is Element of the carrier of X
lim ((S /* p) - (f /* p)) is Element of the carrier of X
(S - 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:]
lim ((S - f) /* p) is Element of the carrier of X
(S - f) | (dom (S - f)) is Relation-like REAL -defined dom (S - f) -defined REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
p 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 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 Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
dom r is V13() V14() V15() Element of bool REAL
(dom f) /\ (dom r) is V13() V14() V15() Element of bool REAL
r | 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:]
f + r is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
(f + r) | 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:]
f - r is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
(f - r) | 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:]
dom (f + r) is V13() V14() V15() Element of bool REAL
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 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 /* 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) + (r /* 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 /. (lim p) is Element of the carrier of X
lim (f /* p) is Element of the carrier of X
r /. (lim p) is Element of the carrier of X
lim (r /* p) is Element of the carrier of X
(f + r) /. (lim p) is Element of the carrier of X
(lim (f /* p)) + (lim (r /* p)) is Element of the carrier of X
lim ((f /* p) + (r /* p)) is Element of the carrier of X
(f + r) /* 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:]
lim ((f + r) /* p) is Element of the carrier of X
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 X -valued Function-like total quasi_total Element of bool [:NAT, the carrier of X:]
r /* 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) - (r /* 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 /. (lim p) is Element of the carrier of X
lim (f /* p) is Element of the carrier of X
r /. (lim p) is Element of the carrier of X
lim (r /* p) is Element of the carrier of X
(f - r) /. (lim p) is Element of the carrier of X
(lim (f /* p)) - (lim (r /* p)) is Element of the carrier of X
- (lim (r /* p)) is Element of the carrier of X
K201(X,(lim (f /* p)),(- (lim (r /* p)))) is Element of the carrier of X
lim ((f /* p) - (r /* p)) is Element of the carrier of X
(f - r) /* 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:]
lim ((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
[:REAL, the carrier of X:] is Relation-like set
bool [:REAL, the carrier of X:] is set
S is set
f is set
S /\ f is set
r is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
dom r is V13() V14() V15() Element of bool REAL
r | 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:]
p is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
dom p is V13() V14() V15() Element of bool REAL
p | 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 + p is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
(r + p) | (S /\ f) is Relation-like REAL -defined S /\ f -defined REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
r - p is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
(r - p) | (S /\ f) is Relation-like REAL -defined S /\ f -defined REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
(dom r) /\ (dom p) is V13() V14() V15() Element of bool REAL
r | (S /\ f) is Relation-like REAL -defined S /\ f -defined REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
p | (S /\ f) is Relation-like REAL -defined S /\ f -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
S is Relation-like REAL -defined the carrier of X -valued Function-like (X) Element of bool [:REAL, the carrier of X:]
f is V11() real ext-real Element of REAL
f (#) 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
dom (f (#) S) is V13() V14() V15() Element of bool REAL
(f (#) 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:]
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
S | (dom S) is Relation-like REAL -defined dom S -defined REAL -defined the carrier of X -valued the carrier of X -valued Function-like (X) Element of bool [:REAL, the carrier of X:]
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
S /. (lim p) is Element of the carrier of X
lim (S /* p) is Element of the carrier of X
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:]
(f (#) S) /. (lim p) is Element of the carrier of X
f * (lim (S /* p)) is Element of the carrier of X
lim (f * (S /* p)) is Element of the carrier of X
(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:]
lim ((f (#) S) /* p) is Element of the carrier of X
p 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 V11() real ext-real Element of REAL
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:]
dom r is V13() V14() V15() Element of bool REAL
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:]
S (#) r is Relation-like REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]
(S (#) 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 (S (#) 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
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
S * (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 /. (lim p) is Element of the carrier of f
lim (r /* p) is Element of the carrier of f
(S (#) r) /. (lim p) is Element of the carrier of f
S * (lim (r /* p)) is Element of the carrier of f
lim (S * (r /* p)) is Element of the carrier of f
(S (#) 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 ((S (#) r) /* p) is Element of the carrier of f
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:]
||.f.|| is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
||.f.|| | X is Relation-like REAL -defined X -defined 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:]
(- 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
dom (||.f.|| | X) is V13() V14() V15() Element of bool REAL
dom (||.f.|| | X) is Element of bool X
bool X is set
dom ||.f.|| is V13() V14() V15() Element of bool REAL
dom (f | X) is Element of bool X
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.|| | X) /* 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:]
(||.f.|| | X) . r is V11() real ext-real Element of REAL
lim ((||.f.|| | X) /* p) is V11() real ext-real Element of REAL
(dom ||.f.||) /\ X is V13() V14() V15() Element of bool REAL
(dom f) /\ X is 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
p . x1 is V11() real ext-real Element of REAL
(f | X) /* 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
||.((f | X) /* 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:]
||.((f | X) /* p).|| . x1 is V11() real ext-real Element of REAL
((f | X) /* p) . x1 is Element of the carrier of S
||.(((f | X) /* p) . x1).|| is V11() real ext-real Element of REAL
(f | X) /. (p . x1) is Element of the carrier of S
||.((f | X) /. (p . x1)).|| is V11() real ext-real Element of REAL
f /. (p . x1) is Element of the carrier of S
||.(f /. (p . x1)).|| is V11() real ext-real Element of REAL
||.f.|| . (p . x1) is V11() real ext-real Element of REAL
(||.f.|| | X) . (p . x1) is V11() real ext-real Element of REAL
((||.f.|| | X) /* p) . x1 is V11() real ext-real Element of REAL
(f | X) /. r is Element of the carrier of S
||.((f | X) /. r).|| is V11() real ext-real Element of REAL
f /. r is Element of the carrier of S
||.(f /. r).|| is V11() real ext-real Element of REAL
||.f.|| . r is V11() real ext-real Element of REAL
lim ((f | X) /* p) is Element of the carrier of S
(- 1) (#) f is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]
((- 1) (#) 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:]
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:]
S | REAL is Relation-like REAL -defined 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
r is V11() real ext-real set
S /. r is Element of the carrier of X
(S /. r) + (S /. r) is Element of the carrier of X
r + r is V11() real ext-real set
S /. (r + r) is Element of the carrier of X
(S /. r) - (S /. r) is Element of the carrier of X
- (S /. r) is Element of the carrier of X
K201(X,(S /. r),(- (S /. r))) is Element of the carrier of X
(S /. r) + ((S /. r) - (S /. r)) is Element of the carrier of X
0. X is V76(X) Element of the carrier of X
(S /. r) + (0. X) is Element of the carrier of X
p is V11() real ext-real set
- p is V11() real ext-real set
p + (- p) is V11() real ext-real set
S /. (p + (- p)) is Element of the carrier of X
S /. p is Element of the carrier of X
S /. (- p) is Element of the carrier of X
(S /. p) + (S /. (- p)) is Element of the carrier of X
- (S /. p) is Element of the carrier of X
p is V11() real ext-real set
x1 is V11() real ext-real set
p - x1 is V11() real ext-real set
S /. (p - x1) is Element of the carrier of X
- x1 is V11() real ext-real set
p + (- x1) is V11() real ext-real set
S /. (p + (- x1)) is Element of the carrier of X
S /. p is Element of the carrier of X
S /. (- x1) is Element of the carrier of X
(S /. p) + (S /. (- x1)) is Element of the carrier of X
S /. x1 is Element of the carrier of X
(S /. p) - (S /. x1) is Element of the carrier of X
- (S /. x1) is Element of the carrier of X
K201(X,(S /. p),(- (S /. x1))) is Element of the carrier of X
p is V11() real ext-real set
x1 is V11() real ext-real Element of REAL
p - f is V11() real ext-real set
S /. f is Element of the carrier of X
s9 is V11() real ext-real set
x1 is V11() real ext-real set
x2 is V11() real ext-real set
x2 - p is V11() real ext-real set
abs (x2 - p) is V11() real ext-real Element of REAL
x2 - (p - f) is V11() real ext-real set
(x2 - (p - f)) - f is V11() real ext-real set
abs ((x2 - (p - f)) - f) is V11() real ext-real Element of REAL
(p - f) + f is V11() real ext-real set
S /. x2 is Element of the carrier of X
S /. p is Element of the carrier of X
(S /. x2) - (S /. p) is Element of the carrier of X
- (S /. p) is Element of the carrier of X
K201(X,(S /. x2),(- (S /. p))) is Element of the carrier of X
||.((S /. x2) - (S /. p)).|| is V11() real ext-real Element of REAL
S /. (p - f) is Element of the carrier of X
(S /. (p - f)) + (S /. f) is Element of the carrier of X
(S /. x2) - ((S /. (p - f)) + (S /. f)) is Element of the carrier of X
- ((S /. (p - f)) + (S /. f)) is Element of the carrier of X
K201(X,(S /. x2),(- ((S /. (p - f)) + (S /. f)))) is Element of the carrier of X
||.((S /. x2) - ((S /. (p - f)) + (S /. f))).|| is V11() real ext-real Element of REAL
(S /. x2) - (S /. (p - f)) is Element of the carrier of X
- (S /. (p - f)) is Element of the carrier of X
K201(X,(S /. x2),(- (S /. (p - f)))) is Element of the carrier of X
((S /. x2) - (S /. (p - f))) - (S /. f) is Element of the carrier of X
- (S /. f) is Element of the carrier of X
K201(X,((S /. x2) - (S /. (p - f))),(- (S /. f))) is Element of the carrier of X
||.(((S /. x2) - (S /. (p - f))) - (S /. f)).|| is V11() real ext-real Element of REAL
S /. (x2 - (p - f)) is Element of the carrier of X
(S /. (x2 - (p - f))) - (S /. f) is Element of the carrier of X
K201(X,(S /. (x2 - (p - f))),(- (S /. f))) is Element of the carrier of X
||.((S /. (x2 - (p - f))) - (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
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:]
rng S is Element of bool the carrier of X
bool the carrier of X is set
[:NAT, the carrier of X:] is Relation-like set
bool [:NAT, the carrier of X:] is set
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:]
rng f is non empty Element of bool the carrier of X
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 set
dom f is non empty V13() V14() V15() V16() V17() V18() Element of bool NAT
f . r is Element of the carrier of X
p is V11() real ext-real Element of REAL
S . p is set
S /. p is Element of 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:]
p is set
rng r 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
r . x1 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:]
lim p is V11() real ext-real Element of REAL
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:]
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
r . x2 is V11() real ext-real Element of REAL
S /. (r . x2) is Element of the carrier of X
f . x2 is Element of the carrier of X
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:]
(S /* r) . x2 is Element of the carrier of X
dom (S | (dom S)) is V13() V14() V15() Element of bool REAL
S /. (lim p) is Element of the carrier of X
lim (S /* p) is Element of the carrier of X
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:]
lim x1 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 V13() V14() V15() Element of bool REAL
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:]
S .: f is Element of bool the carrier of X
bool the carrier of X is set
(S | f) | 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 f
bool f is set
(dom S) /\ f is V13() V14() V15() Element of bool REAL
rng (S | f) is Element of bool 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 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:]
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:]
dom (f | X) is Element of bool X
bool X is set
r is V11() real ext-real set
p is V11() real ext-real set
f /. p is Element of the carrier of S
x1 is V11() real ext-real set
f /. x1 is Element of the carrier of S
(f /. p) - (f /. x1) is Element of the carrier of S
- (f /. x1) is Element of the carrier of S
K201(S,(f /. p),(- (f /. x1))) is Element of the carrier of S
||.((f /. p) - (f /. x1)).|| is V11() real ext-real Element of REAL
p - x1 is V11() real ext-real set
abs (p - x1) is V11() real ext-real Element of REAL
r * (abs (p - x1)) is V11() real ext-real Element of REAL
(f | X) /. p is Element of the carrier of S
(f | X) /. x1 is Element of the carrier of S
r is V11() real ext-real set
dom (f | X) is V13() V14() V15() Element of bool REAL
p is V11() real ext-real set
(f | X) /. p is Element of the carrier of S
x1 is V11() real ext-real set
(f | X) /. x1 is Element of the carrier of S
((f | X) /. p) - ((f | X) /. x1) is Element of the carrier of S
- ((f | X) /. x1) is Element of the carrier of S
K201(S,((f | X) /. p),(- ((f | X) /. x1))) is Element of the carrier of S
||.(((f | X) /. p) - ((f | X) /. x1)).|| is V11() real ext-real Element of REAL
p - x1 is V11() real ext-real set
abs (p - x1) is V11() real ext-real Element of REAL
r * (abs (p - x1)) is V11() real ext-real Element of REAL
f /. p is Element of the carrier of S
f /. x1 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
r is V11() real ext-real set
S /. f is Element of the carrier of X
S /. r is Element of the carrier of X
(S /. f) - (S /. r) is Element of the carrier of X
- (S /. r) is Element of the carrier of X
K201(X,(S /. f),(- (S /. r))) is Element of the carrier of X
||.((S /. f) - (S /. r)).|| is V11() real ext-real Element of REAL
f - r is V11() real ext-real set
abs (f - r) is V11() real ext-real Element of REAL
1 * (abs (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
the 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 REAL -defined the carrier of X -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing (X) (X) Element of bool [:REAL, the carrier of X:] 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 REAL -defined the carrier of X -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing (X) (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:]
dom S is V13() V14() V15() Element of bool REAL
r is V11() real ext-real set
p is V11() real ext-real set
dom (S | f) is Element of bool f
bool f is set
x1 is V11() real ext-real set
S /. p is Element of the carrier of X
S /. x1 is Element of the carrier of X
(S /. p) - (S /. x1) is Element of the carrier of X
- (S /. x1) is Element of the carrier of X
K201(X,(S /. p),(- (S /. x1))) is Element of the carrier of X
||.((S /. p) - (S /. x1)).|| is V11() real ext-real Element of REAL
p - x1 is V11() real ext-real set
abs (p - x1) is V11() real ext-real Element of REAL
r * (abs (p - x1)) is V11() real ext-real Element of REAL
p 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 (X) Element of bool [:REAL, the carrier of X:]
f is Relation-like REAL -defined the carrier of X -valued Function-like (X) 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:]
dom S is V13() V14() V15() Element of bool REAL
dom f is V13() V14() V15() Element of bool REAL
(dom S) /\ (dom f) is V13() V14() V15() Element of bool REAL
S | ((dom S) /\ (dom f)) is Relation-like REAL -defined (dom S) /\ (dom f) -defined REAL -defined the carrier of X -valued the carrier of X -valued Function-like (X) Element of bool [:REAL, the carrier of X:]
dom (S | ((dom S) /\ (dom f))) is V13() V14() V15() Element of bool ((dom S) /\ (dom f))
bool ((dom S) /\ (dom f)) is set
x1 is V11() real ext-real set
f | ((dom S) /\ (dom f)) is Relation-like REAL -defined (dom S) /\ (dom f) -defined REAL -defined the carrier of X -valued the carrier of X -valued Function-like (X) Element of bool [:REAL, the carrier of X:]
dom (f | ((dom S) /\ (dom f))) is V13() V14() V15() Element of bool ((dom S) /\ (dom f))
x2 is V11() real ext-real set
x1 + x2 is V11() real ext-real set
s9 is V11() real ext-real set
x1 is V11() real ext-real set
dom (S + f) is V13() V14() V15() Element of bool REAL
x2 is V11() real ext-real set
(S + f) /. x1 is Element of the carrier of X
(S + f) /. x2 is Element of the carrier of X
((S + f) /. x1) - ((S + f) /. x2) is Element of the carrier of X
- ((S + f) /. x2) is Element of the carrier of X
K201(X,((S + f) /. x1),(- ((S + f) /. x2))) is Element of the carrier of X
||.(((S + f) /. x1) - ((S + f) /. x2)).|| is V11() real ext-real Element of REAL
S /. x1 is Element of the carrier of X
f /. x1 is Element of the carrier of X
(S /. x1) + (f /. x1) is Element of the carrier of X
((S /. x1) + (f /. x1)) - ((S + f) /. x2) is Element of the carrier of X
K201(X,((S /. x1) + (f /. x1)),(- ((S + f) /. x2))) is Element of the carrier of X
||.(((S /. x1) + (f /. x1)) - ((S + f) /. x2)).|| is V11() real ext-real Element of REAL
S /. x2 is Element of the carrier of X
f /. x2 is Element of the carrier of X
(S /. x2) + (f /. x2) is Element of the carrier of X
((S /. x1) + (f /. x1)) - ((S /. x2) + (f /. x2)) is Element of the carrier of X
- ((S /. x2) + (f /. x2)) is Element of the carrier of X
K201(X,((S /. x1) + (f /. x1)),(- ((S /. x2) + (f /. x2)))) is Element of the carrier of X
||.(((S /. x1) + (f /. x1)) - ((S /. x2) + (f /. x2))).|| is V11() real ext-real Element of REAL
(f /. x1) - ((S /. x2) + (f /. x2)) is Element of the carrier of X
K201(X,(f /. x1),(- ((S /. x2) + (f /. x2)))) is Element of the carrier of X
(S /. x1) + ((f /. x1) - ((S /. x2) + (f /. x2))) is Element of the carrier of X
||.((S /. x1) + ((f /. x1) - ((S /. x2) + (f /. x2)))).|| is V11() real ext-real Element of REAL
(f /. x1) - (S /. x2) is Element of the carrier of X
- (S /. x2) is Element of the carrier of X
K201(X,(f /. x1),(- (S /. x2))) is Element of the carrier of X
((f /. x1) - (S /. x2)) - (f /. x2) is Element of the carrier of X
- (f /. x2) is Element of the carrier of X
K201(X,((f /. x1) - (S /. x2)),(- (f /. x2))) is Element of the carrier of X
(S /. x1) + (((f /. x1) - (S /. x2)) - (f /. x2)) is Element of the carrier of X
||.((S /. x1) + (((f /. x1) - (S /. x2)) - (f /. x2))).|| is V11() real ext-real Element of REAL
(- (S /. x2)) + (f /. x1) is Element of the carrier of X
((- (S /. x2)) + (f /. x1)) - (f /. x2) is Element of the carrier of X
K201(X,((- (S /. x2)) + (f /. x1)),(- (f /. x2))) is Element of the carrier of X
(S /. x1) + (((- (S /. x2)) + (f /. x1)) - (f /. x2)) is Element of the carrier of X
||.((S /. x1) + (((- (S /. x2)) + (f /. x1)) - (f /. x2))).|| is V11() real ext-real Element of REAL
(f /. x1) - (f /. x2) is Element of the carrier of X
K201(X,(f /. x1),(- (f /. x2))) is Element of the carrier of X
(- (S /. x2)) + ((f /. x1) - (f /. x2)) is Element of the carrier of X
(S /. x1) + ((- (S /. x2)) + ((f /. x1) - (f /. x2))) is Element of the carrier of X
||.((S /. x1) + ((- (S /. x2)) + ((f /. x1) - (f /. x2)))).|| is V11() real ext-real Element of REAL
(S /. x1) - (S /. x2) is Element of the carrier of X
K201(X,(S /. x1),(- (S /. x2))) is Element of the carrier of X
((S /. x1) - (S /. x2)) + ((f /. x1) - (f /. x2)) is Element of the carrier of X
||.(((S /. x1) - (S /. x2)) + ((f /. x1) - (f /. x2))).|| is V11() real ext-real Element of REAL
||.((S /. x1) - (S /. x2)).|| is V11() real ext-real Element of REAL
||.((f /. x1) - (f /. x2)).|| is V11() real ext-real Element of REAL
||.((S /. x1) - (S /. x2)).|| + ||.((f /. x1) - (f /. x2)).|| is V11() real ext-real Element of REAL
(dom f) /\ ((dom S) /\ (dom f)) is V13() V14() V15() Element of bool REAL
(dom f) /\ (dom f) is V13() V14() V15() Element of bool REAL
((dom f) /\ (dom f)) /\ (dom S) is V13() V14() V15() Element of bool REAL
x1 - x2 is V11() real ext-real set
abs (x1 - x2) is V11() real ext-real Element of REAL
x2 * (abs (x1 - x2)) is V11() real ext-real Element of REAL
(dom S) /\ ((dom S) /\ (dom f)) is V13() V14() V15() Element of bool REAL
(dom S) /\ (dom S) is V13() V14() V15() Element of bool REAL
((dom S) /\ (dom S)) /\ (dom f) is V13() V14() V15() Element of bool REAL
x1 * (abs (x1 - x2)) is V11() real ext-real Element of REAL
(x1 * (abs (x1 - x2))) + (x2 * (abs (x1 - x2))) is V11() real ext-real Element of REAL
s9 * (abs (x1 - x2)) is V11() real ext-real Element of REAL
s9 is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
x1 is V11() real ext-real set
S - f 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
dom f is V13() V14() V15() Element of bool REAL
(dom S) /\ (dom f) is V13() V14() V15() Element of bool REAL
S | ((dom S) /\ (dom f)) is Relation-like REAL -defined (dom S) /\ (dom f) -defined REAL -defined the carrier of X -valued the carrier of X -valued Function-like (X) Element of bool [:REAL, the carrier of X:]
dom (S | ((dom S) /\ (dom f))) is V13() V14() V15() Element of bool ((dom S) /\ (dom f))
bool ((dom S) /\ (dom f)) is set
x1 is V11() real ext-real set
f | ((dom S) /\ (dom f)) is Relation-like REAL -defined (dom S) /\ (dom f) -defined REAL -defined the carrier of X -valued the carrier of X -valued Function-like (X) Element of bool [:REAL, the carrier of X:]
dom (f | ((dom S) /\ (dom f))) is V13() V14() V15() Element of bool ((dom S) /\ (dom f))
x2 is V11() real ext-real set
x1 + x2 is V11() real ext-real set
s9 is V11() real ext-real set
x1 is V11() real ext-real set
dom (S - f) is V13() V14() V15() Element of bool REAL
x2 is V11() real ext-real set
(S - f) /. x1 is Element of the carrier of X
(S - f) /. x2 is Element of the carrier of X
((S - f) /. x1) - ((S - f) /. x2) is Element of the carrier of X
- ((S - f) /. x2) is Element of the carrier of X
K201(X,((S - f) /. x1),(- ((S - f) /. x2))) is Element of the carrier of X
||.(((S - f) /. x1) - ((S - f) /. x2)).|| is V11() real ext-real Element of REAL
S /. x1 is Element of the carrier of X
f /. x1 is Element of the carrier of X
(S /. x1) - (f /. x1) is Element of the carrier of X
- (f /. x1) is Element of the carrier of X
K201(X,(S /. x1),(- (f /. x1))) is Element of the carrier of X
((S /. x1) - (f /. x1)) - ((S - f) /. x2) is Element of the carrier of X
K201(X,((S /. x1) - (f /. x1)),(- ((S - f) /. x2))) is Element of the carrier of X
||.(((S /. x1) - (f /. x1)) - ((S - f) /. x2)).|| is V11() real ext-real Element of REAL
S /. x2 is Element of the carrier of X
f /. x2 is Element of the carrier of X
(S /. x2) - (f /. x2) is Element of the carrier of X
- (f /. x2) is Element of the carrier of X
K201(X,(S /. x2),(- (f /. x2))) is Element of the carrier of X
((S /. x1) - (f /. x1)) - ((S /. x2) - (f /. x2)) is Element of the carrier of X
- ((S /. x2) - (f /. x2)) is Element of the carrier of X
K201(X,((S /. x1) - (f /. x1)),(- ((S /. x2) - (f /. x2)))) is Element of the carrier of X
||.(((S /. x1) - (f /. x1)) - ((S /. x2) - (f /. x2))).|| is V11() real ext-real Element of REAL
(f /. x1) + ((S /. x2) - (f /. x2)) is Element of the carrier of X
(S /. x1) - ((f /. x1) + ((S /. x2) - (f /. x2))) is Element of the carrier of X
- ((f /. x1) + ((S /. x2) - (f /. x2))) is Element of the carrier of X
K201(X,(S /. x1),(- ((f /. x1) + ((S /. x2) - (f /. x2))))) is Element of the carrier of X
||.((S /. x1) - ((f /. x1) + ((S /. x2) - (f /. x2)))).|| is V11() real ext-real Element of REAL
(S /. x2) + (f /. x1) is Element of the carrier of X
((S /. x2) + (f /. x1)) - (f /. x2) is Element of the carrier of X
K201(X,((S /. x2) + (f /. x1)),(- (f /. x2))) is Element of the carrier of X
(S /. x1) - (((S /. x2) + (f /. x1)) - (f /. x2)) is Element of the carrier of X
- (((S /. x2) + (f /. x1)) - (f /. x2)) is Element of the carrier of X
K201(X,(S /. x1),(- (((S /. x2) + (f /. x1)) - (f /. x2)))) is Element of the carrier of X
||.((S /. x1) - (((S /. x2) + (f /. x1)) - (f /. x2))).|| is V11() real ext-real Element of REAL
(f /. x1) - (f /. x2) is Element of the carrier of X
K201(X,(f /. x1),(- (f /. x2))) is Element of the carrier of X
(S /. x2) + ((f /. x1) - (f /. x2)) is Element of the carrier of X
(S /. x1) - ((S /. x2) + ((f /. x1) - (f /. x2))) is Element of the carrier of X
- ((S /. x2) + ((f /. x1) - (f /. x2))) is Element of the carrier of X
K201(X,(S /. x1),(- ((S /. x2) + ((f /. x1) - (f /. x2))))) is Element of the carrier of X
||.((S /. x1) - ((S /. x2) + ((f /. x1) - (f /. x2)))).|| is V11() real ext-real Element of REAL
(S /. x1) - (S /. x2) is Element of the carrier of X
- (S /. x2) is Element of the carrier of X
K201(X,(S /. x1),(- (S /. x2))) is Element of the carrier of X
((S /. x1) - (S /. x2)) - ((f /. x1) - (f /. x2)) is Element of the carrier of X
- ((f /. x1) - (f /. x2)) is Element of the carrier of X
K201(X,((S /. x1) - (S /. x2)),(- ((f /. x1) - (f /. x2)))) is Element of the carrier of X
||.(((S /. x1) - (S /. x2)) - ((f /. x1) - (f /. x2))).|| is V11() real ext-real Element of REAL
||.((S /. x1) - (S /. x2)).|| is V11() real ext-real Element of REAL
||.((f /. x1) - (f /. x2)).|| is V11() real ext-real Element of REAL
||.((S /. x1) - (S /. x2)).|| + ||.((f /. x1) - (f /. x2)).|| is V11() real ext-real Element of REAL
(dom f) /\ ((dom S) /\ (dom f)) is V13() V14() V15() Element of bool REAL
(dom f) /\ (dom f) is V13() V14() V15() Element of bool REAL
((dom f) /\ (dom f)) /\ (dom S) is V13() V14() V15() Element of bool REAL
x1 - x2 is V11() real ext-real set
abs (x1 - x2) is V11() real ext-real Element of REAL
x2 * (abs (x1 - x2)) is V11() real ext-real Element of REAL
(dom S) /\ ((dom S) /\ (dom f)) is V13() V14() V15() Element of bool REAL
(dom S) /\ (dom S) is V13() V14() V15() Element of bool REAL
((dom S) /\ (dom S)) /\ (dom f) is V13() V14() V15() Element of bool REAL
x1 * (abs (x1 - x2)) is V11() real ext-real Element of REAL
(x1 * (abs (x1 - x2))) + (x2 * (abs (x1 - x2))) is V11() real ext-real Element of REAL
s9 * (abs (x1 - x2)) is V11() real ext-real Element of REAL
s9 is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
x1 is V11() real ext-real set
X is set
S is set
X /\ 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:]
p is Relation-like REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]
p | 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 + p is Relation-like REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]
(r + p) | (X /\ S) is Relation-like REAL -defined X /\ 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 X /\ S -defined REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]
(r | X) | (X /\ S) is Relation-like REAL -defined X /\ S -defined REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]
p | (X /\ S) is Relation-like REAL -defined X /\ S -defined REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]
(p | S) | (X /\ S) is Relation-like REAL -defined X /\ S -defined REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]
(r | (X /\ S)) + (p | (X /\ S)) is Relation-like REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]
X is set
S is set
X /\ 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:]
p is Relation-like REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]
p | 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 - p is Relation-like REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]
(r - p) | (X /\ S) is Relation-like REAL -defined X /\ 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 X /\ S -defined REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]
(r | X) | (X /\ S) is Relation-like REAL -defined X /\ S -defined REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]
p | (X /\ S) is Relation-like REAL -defined X /\ S -defined REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]
(p | S) | (X /\ S) is Relation-like REAL -defined X /\ S -defined REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]
(r | (X /\ S)) - (p | (X /\ S)) is Relation-like 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 (X) Element of bool [:REAL, the carrier of X:]
f is V11() real ext-real Element of REAL
f (#) 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
r is V11() real ext-real set
p is V11() real ext-real set
x1 is V11() real ext-real set
dom (f (#) S) is V13() V14() V15() Element of bool REAL
x2 is V11() real ext-real set
x1 - x2 is V11() real ext-real set
abs (x1 - x2) is V11() real ext-real Element of REAL
(f (#) S) /. x1 is Element of the carrier of X
(f (#) S) /. x2 is Element of the carrier of X
((f (#) S) /. x1) - ((f (#) S) /. x2) is Element of the carrier of X
- ((f (#) S) /. x2) is Element of the carrier of X
K201(X,((f (#) S) /. x1),(- ((f (#) S) /. x2))) is Element of the carrier of X
||.(((f (#) S) /. x1) - ((f (#) S) /. x2)).|| is V11() real ext-real Element of REAL
S /. x1 is Element of the carrier of X
f * (S /. x1) is Element of the carrier of X
(f * (S /. x1)) - ((f (#) S) /. x2) is Element of the carrier of X
K201(X,(f * (S /. x1)),(- ((f (#) S) /. x2))) is Element of the carrier of X
||.((f * (S /. x1)) - ((f (#) S) /. x2)).|| is V11() real ext-real Element of REAL
S /. x2 is Element of the carrier of X
f * (S /. x2) is Element of the carrier of X
(f * (S /. x1)) - (f * (S /. x2)) is Element of the carrier of X
- (f * (S /. x2)) is Element of the carrier of X
K201(X,(f * (S /. x1)),(- (f * (S /. x2)))) is Element of the carrier of X
||.((f * (S /. x1)) - (f * (S /. x2))).|| is V11() real ext-real Element of REAL
0. X is V76(X) Element of the carrier of X
(0. X) - (f * (S /. x2)) is Element of the carrier of X
K201(X,(0. X),(- (f * (S /. x2)))) is Element of the carrier of X
||.((0. X) - (f * (S /. x2))).|| is V11() real ext-real Element of REAL
(0. X) - (0. X) is Element of the carrier of X
- (0. X) is Element of the carrier of X
K201(X,(0. X),(- (0. X))) is Element of the carrier of X
||.((0. X) - (0. X)).|| is V11() real ext-real Element of REAL
p * (abs (x1 - x2)) is V11() real ext-real Element of REAL
p is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
x1 is V11() real ext-real set
abs f is V11() real ext-real Element of REAL
(abs f) * r is V11() real ext-real Element of REAL
0 * 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
dom (f (#) S) is V13() V14() V15() Element of bool REAL
x2 is V11() real ext-real set
(f (#) S) /. x1 is Element of the carrier of X
(f (#) S) /. x2 is Element of the carrier of X
((f (#) S) /. x1) - ((f (#) S) /. x2) is Element of the carrier of X
- ((f (#) S) /. x2) is Element of the carrier of X
K201(X,((f (#) S) /. x1),(- ((f (#) S) /. x2))) is Element of the carrier of X
||.(((f (#) S) /. x1) - ((f (#) S) /. x2)).|| is V11() real ext-real Element of REAL
S /. x1 is Element of the carrier of X
f * (S /. x1) is Element of the carrier of X
(f * (S /. x1)) - ((f (#) S) /. x2) is Element of the carrier of X
K201(X,(f * (S /. x1)),(- ((f (#) S) /. x2))) is Element of the carrier of X
||.((f * (S /. x1)) - ((f (#) S) /. x2)).|| is V11() real ext-real Element of REAL
S /. x2 is Element of the carrier of X
f * (S /. x2) is Element of the carrier of X
(f * (S /. x1)) - (f * (S /. x2)) is Element of the carrier of X
- (f * (S /. x2)) is Element of the carrier of X
K201(X,(f * (S /. x1)),(- (f * (S /. x2)))) is Element of the carrier of X
||.((f * (S /. x1)) - (f * (S /. x2))).|| is V11() real ext-real Element of REAL
(S /. x1) - (S /. x2) is Element of the carrier of X
- (S /. x2) is Element of the carrier of X
K201(X,(S /. x1),(- (S /. x2))) is Element of the carrier of X
f * ((S /. x1) - (S /. x2)) is Element of the carrier of X
||.(f * ((S /. x1) - (S /. x2))).|| is V11() real ext-real Element of REAL
||.((S /. x1) - (S /. x2)).|| is V11() real ext-real Element of REAL
(abs f) * ||.((S /. x1) - (S /. x2)).|| is V11() real ext-real Element of REAL
x1 - x2 is V11() real ext-real set
abs (x1 - x2) is V11() real ext-real Element of REAL
r * (abs (x1 - x2)) is V11() real ext-real Element of REAL
(abs f) * (r * (abs (x1 - x2))) is V11() real ext-real Element of REAL
p * (abs (x1 - x2)) is V11() real ext-real Element of REAL
p is Relation-like REAL -defined the carrier of X -valued Function-like Element of bool [:REAL, the carrier of X:]
x1 is V11() real ext-real Element of REAL
X is set
S is V11() real ext-real Element of REAL
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
S (#) r is Relation-like REAL -defined the carrier of f -valued Function-like Element of bool [:REAL, the carrier of f:]
(S (#) 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:]
S (#) (r | X) is Relation-like 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 (X) Element of bool [:REAL, the carrier of X:]
||.S.|| is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom S is V13() V14() V15() Element of bool REAL
f is V11() real ext-real set
r is V11() real ext-real set
dom ||.S.|| is V13() V14() V15() Element of bool REAL
p is V11() real ext-real set
S /. r is Element of the carrier of X
S /. p is Element of the carrier of X
(S /. r) - (S /. p) is Element of the carrier of X
- (S /. p) is Element of the carrier of X
K201(X,(S /. r),(- (S /. p))) is Element of the carrier of X
||.((S /. r) - (S /. p)).|| is V11() real ext-real Element of REAL
r - p is V11() real ext-real set
abs (r - p) is V11() real ext-real Element of REAL
f * (abs (r - p)) is V11() real ext-real Element of REAL
||.S.|| . r is V11() real ext-real Element of REAL
||.S.|| . p is V11() real ext-real Element of REAL
(||.S.|| . r) - (||.S.|| . p) is V11() real ext-real Element of REAL
abs ((||.S.|| . r) - (||.S.|| . p)) is V11() real ext-real Element of REAL
||.(S /. r).|| is V11() real ext-real Element of REAL
||.(S /. r).|| - (||.S.|| . p) is V11() real ext-real Element of REAL
abs (||.(S /. r).|| - (||.S.|| . p)) is V11() real ext-real Element of REAL
||.(S /. p).|| is V11() real ext-real Element of REAL
||.(S /. r).|| - ||.(S /. p).|| is V11() real ext-real Element of REAL
abs (||.(S /. r).|| - ||.(S /. p).||) is V11() real ext-real Element of REAL
r is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
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:]
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:]
- (f | X) is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]
- f is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]
(- 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:]
||.f.|| is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
||.f.|| | X is Relation-like REAL -defined X -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(- 1) (#) (f | X) is Relation-like REAL -defined the carrier of S -valued Function-like Element of bool [:REAL, the carrier of S:]
||.(f | X).|| is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,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:]
f is V11() real ext-real set
dom S is V13() V14() V15() Element of bool REAL
r is V11() real ext-real set
S /. f is Element of the carrier of X
S . f is set
S . r is set
S /. r is Element of the carrier of X
(S /. f) - (S /. r) is Element of the carrier of X
- (S /. r) is Element of the carrier of X
K201(X,(S /. f),(- (S /. r))) is Element of the carrier of X
||.((S /. f) - (S /. r)).|| is V11() real ext-real Element of REAL
f - r is V11() real ext-real set
abs (f - r) is V11() real ext-real Element of REAL
1 * (abs (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:]
dom S is V13() V14() V15() Element of bool REAL
r is V11() real ext-real set
p is V11() real ext-real set
S /. p is Element of the carrier of X
x1 is V11() real ext-real Element of REAL
x1 / r is V11() real ext-real Element of COMPLEX
s9 is V11() real ext-real Element of COMPLEX
x1 is V11() real ext-real set
x1 - p is V11() real ext-real set
abs (x1 - p) is V11() real ext-real Element of REAL
(x1 / r) * r is V11() real ext-real set
r * (abs (x1 - p)) is V11() real ext-real Element of REAL
S /. x1 is Element of the carrier of X
(S /. x1) - (S /. p) is Element of the carrier of X
- (S /. p) is Element of the carrier of X
K201(X,(S /. x1),(- (S /. p))) is Element of the carrier of X
||.((S /. x1) - (S /. p)).|| is V11() real ext-real Element of REAL
r " is V11() real ext-real set
x1 * (r ") is V11() real ext-real Element of REAL
x1 is V11() real ext-real set
x1 - p is V11() real ext-real set
abs (x1 - p) is V11() real ext-real Element of REAL
S /. x1 is Element of the carrier of X
(S /. x1) - (S /. p) is Element of the carrier of X
K201(X,(S /. x1),(- (S /. p))) is Element of the carrier of X
||.((S /. x1) - (S /. p)).|| 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:]
rng S is Element of bool the carrier of X
bool the carrier of X is set
f is Element of the carrier of X
{f} is non empty trivial set
r is V11() real ext-real set
dom S is V13() V14() V15() Element of bool REAL
p is V11() real ext-real set
S . p is set
S /. p is Element of the carrier of X
S . r is set
S /. r is Element of the carrier of X
(S /. r) - (S /. p) is Element of the carrier of X
- (S /. p) is Element of the carrier of X
K201(X,(S /. r),(- (S /. p))) is Element of the carrier of X
||.((S /. r) - (S /. p)).|| is V11() real ext-real Element of REAL
r - p is V11() real ext-real set
abs (r - p) is V11() real ext-real Element of REAL
1 * (abs (r - p)) is V11() real ext-real Element of REAL
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:]
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 Element of the carrier of S
p is Element of the carrier of S
x1 is V11() real ext-real set
dom (f | X) is Element of bool X
bool X is set
x2 is V11() real ext-real set
f /. x2 is Element of the carrier of S
x2 * r is Element of the carrier of S
(x2 * r) + p is Element of the carrier of S
x1 - x2 is V11() real ext-real set
abs (x1 - x2) is V11() real ext-real Element of REAL
f /. x1 is Element of the carrier of S
x1 * r is Element of the carrier of S
(x1 * r) + p is Element of the carrier of S
(f /. x1) - (f /. x2) is Element of the carrier of S
- (f /. x2) is Element of the carrier of S
K201(S,(f /. x1),(- (f /. x2))) is Element of the carrier of S
||.((f /. x1) - (f /. x2)).|| is V11() real ext-real Element of REAL
p + (x2 * r) is Element of the carrier of S
p - (p + (x2 * r)) is Element of the carrier of S
- (p + (x2 * r)) is Element of the carrier of S
K201(S,p,(- (p + (x2 * r)))) is Element of the carrier of S
(x1 * r) + (p - (p + (x2 * r))) is Element of the carrier of S
||.((x1 * r) + (p - (p + (x2 * r)))).|| is V11() real ext-real Element of REAL
p - p is Element of the carrier of S
- p is Element of the carrier of S
K201(S,p,(- p)) is Element of the carrier of S
(p - p) - (x2 * r) is Element of the carrier of S
- (x2 * r) is Element of the carrier of S
K201(S,(p - p),(- (x2 * r))) is Element of the carrier of S
(x1 * r) + ((p - p) - (x2 * r)) is Element of the carrier of S
||.((x1 * r) + ((p - p) - (x2 * r))).|| is V11() real ext-real Element of REAL
0. S is V76(S) Element of the carrier of S
(0. S) - (x2 * r) is Element of the carrier of S
K201(S,(0. S),(- (x2 * r))) is Element of the carrier of S
(x1 * r) + ((0. S) - (x2 * r)) is Element of the carrier of S
||.((x1 * r) + ((0. S) - (x2 * r))).|| is V11() real ext-real Element of REAL
(x1 * r) - (x2 * r) is Element of the carrier of S
K201(S,(x1 * r),(- (x2 * r))) is Element of the carrier of S
||.((x1 * r) - (x2 * r)).|| is V11() real ext-real Element of REAL
(x1 - x2) * r is Element of the carrier of S
||.((x1 - x2) * r).|| is V11() real ext-real Element of REAL
||.r.|| is V11() real ext-real Element of REAL
(abs (x1 - x2)) * ||.r.|| is V11() real ext-real Element of REAL
||.((f /. x1) - (f /. x2)).|| + 0 is V11() real ext-real Element of REAL
||.r.|| * (abs (x1 - x2)) is V11() real ext-real Element of REAL
1 * (abs (x1 - x2)) is V11() real ext-real Element of REAL
(||.r.|| * (abs (x1 - x2))) + (1 * (abs (x1 - x2))) is V11() real ext-real Element of REAL
||.r.|| + 1 is V11() real ext-real Element of REAL
(||.r.|| + 1) * (abs (x1 - x2)) is V11() real ext-real Element of REAL
0 + 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 set