:: NDIFF_5 semantic presentation

REAL is non empty non trivial V49() complex-membered ext-real-membered real-membered V167() non bounded_below non bounded_above V251() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V49() cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V167() countable denumerable left_end bounded_below Element of K6(REAL)
K6(REAL) is non trivial V49() set
COMPLEX is non empty non trivial V49() complex-membered V167() set
K7(REAL,REAL) is non trivial Relation-like complex-valued ext-real-valued real-valued V49() set
K6(K7(REAL,REAL)) is non trivial V49() set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal V49() cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V167() countable denumerable left_end bounded_below set
K6(omega) is non trivial V49() set
K6(NAT) is non trivial V49() set
K7(NAT,REAL) is non trivial Relation-like complex-valued ext-real-valued real-valued V49() set
K6(K7(NAT,REAL)) is non trivial V49() set
K206() is non empty set
K7(K206(),K206()) is Relation-like set
K7(K7(K206(),K206()),K206()) is Relation-like set
K6(K7(K7(K206(),K206()),K206())) is set
K7(REAL,K206()) is non trivial Relation-like V49() set
K7(K7(REAL,K206()),K206()) is non trivial Relation-like V49() set
K6(K7(K7(REAL,K206()),K206())) is non trivial V49() set
K212() is RLSStruct
the carrier of K212() is set
K6( the carrier of K212()) is set
K216() is Element of K6( the carrier of K212())
K7(K216(),K216()) is Relation-like set
K7(K7(K216(),K216()),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(K7(K216(),K216()),REAL)) is set
RAT is non empty non trivial V49() complex-membered ext-real-membered real-membered rational-membered V167() set
INT is non empty non trivial V49() complex-membered ext-real-membered real-membered rational-membered integer-membered V167() set
K7(COMPLEX,COMPLEX) is non trivial Relation-like complex-valued V49() set
K6(K7(COMPLEX,COMPLEX)) is non trivial V49() set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is non trivial Relation-like complex-valued V49() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non trivial V49() set
K7(K7(REAL,REAL),REAL) is non trivial Relation-like complex-valued ext-real-valued real-valued V49() set
K6(K7(K7(REAL,REAL),REAL)) is non trivial V49() set
K7(RAT,RAT) is non trivial Relation-like RAT -valued complex-valued ext-real-valued real-valued V49() set
K6(K7(RAT,RAT)) is non trivial V49() set
K7(K7(RAT,RAT),RAT) is non trivial Relation-like RAT -valued complex-valued ext-real-valued real-valued V49() set
K6(K7(K7(RAT,RAT),RAT)) is non trivial V49() set
K7(INT,INT) is non trivial Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued V49() set
K6(K7(INT,INT)) is non trivial V49() set
K7(K7(INT,INT),INT) is non trivial Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued V49() set
K6(K7(K7(INT,INT),INT)) is non trivial V49() set
K7(NAT,NAT) is non trivial Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued V49() set
K7(K7(NAT,NAT),NAT) is non trivial Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued V49() set
K6(K7(K7(NAT,NAT),NAT)) is non trivial V49() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable left_end right_end bounded_below bounded_above real-bounded Element of NAT
K7(1,1) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued V49() countable set
K6(K7(1,1)) is V49() V53() countable set
K7(K7(1,1),1) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued V49() countable set
K6(K7(K7(1,1),1)) is V49() V53() countable set
K7(K7(1,1),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(K7(1,1),REAL)) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable left_end right_end bounded_below bounded_above real-bounded Element of NAT
K7(2,2) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued V49() countable set
K7(K7(2,2),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(K7(2,2),REAL)) is set
TOP-REAL 2 is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like strict constituted-Functions constituted-FinSeqs RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued V49() V50() V53() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V134() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V167() Cardinal-yielding countable bounded_below bounded_above real-bounded V251() set
ExtREAL is non empty ext-real-membered V251() set
K7(COMPLEX,REAL) is non trivial Relation-like complex-valued ext-real-valued real-valued V49() set
K6(K7(COMPLEX,REAL)) is non trivial V49() set
K764() is non empty strict multMagma
the carrier of K764() is non empty set
<REAL,+> is non empty strict V135() V136() V137() V139() left-invertible right-invertible invertible left-cancelable right-cancelable V277() multMagma
K442() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
multMagma(# REAL,K442() #) is strict multMagma
K770() is non empty strict V137() V139() left-cancelable right-cancelable V277() SubStr of <REAL,+>
<NAT,+> is non empty strict V135() V137() V139() left-cancelable right-cancelable V277() uniquely-decomposable SubStr of K770()
<REAL,*> is non empty strict V135() V137() V139() multMagma
K444() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
multMagma(# REAL,K444() #) is strict multMagma
<NAT,*> is non empty strict V135() V137() V139() uniquely-decomposable SubStr of <REAL,*>
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued V49() V50() V53() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V132() Function-yielding V134() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V167() Cardinal-yielding countable bounded_below bounded_above real-bounded V251() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable left_end right_end bounded_below bounded_above real-bounded Element of NAT
- 1 is non empty V11() real ext-real non positive negative Element of REAL
Seg 1 is non empty trivial V49() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty trivial V49() V53() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable left_end right_end bounded_below bounded_above real-bounded set
Seg 2 is non empty V49() 2 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{1,2} is non empty V49() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable left_end right_end bounded_below bounded_above real-bounded set
<*> REAL is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued V49() V50() V53() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V134() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V167() Cardinal-yielding countable bounded_below bounded_above real-bounded V251() FinSequence of REAL
Sum (<*> REAL) is V11() real ext-real Element of REAL
G is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
the carrier of G is non empty non trivial set
K7(REAL, the carrier of G) is non trivial Relation-like V49() set
K6(K7(REAL, the carrier of G)) is non trivial V49() set
F is non empty Relation-like REAL -defined the carrier of G -valued Function-like total quasi_total Element of K6(K7(REAL, the carrier of G))
dom F is non empty complex-membered ext-real-membered real-membered Element of K6(REAL)
f is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable left_end right_end bounded_below bounded_above real-bounded Element of NAT
1 / (X + 1) is non empty V11() real ext-real positive non negative V160() Element of RAT
K39((X + 1)) is non empty V11() real ext-real positive non negative set
K37(1,K39((X + 1))) is non empty V11() real ext-real positive non negative set
X is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
m is V11() real ext-real set
m " is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
y0 is V11() real ext-real set
i + y0 is V11() real ext-real Element of REAL
i0 is V11() real ext-real set
(m ") + i0 is V11() real ext-real Element of REAL
1 / (m ") is V11() real ext-real Element of REAL
K39((m ")) is V11() real ext-real set
K37(1,K39((m "))) is V11() real ext-real set
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable left_end right_end bounded_below bounded_above real-bounded Element of NAT
1 / (i + 1) is non empty V11() real ext-real positive non negative V160() Element of RAT
K39((i + 1)) is non empty V11() real ext-real positive non negative set
K37(1,K39((i + 1))) is non empty V11() real ext-real positive non negative set
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable left_end right_end bounded_below bounded_above real-bounded Element of NAT
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable left_end right_end bounded_below bounded_above real-bounded Element of NAT
1 / (s + 1) is non empty V11() real ext-real positive non negative V160() Element of RAT
K39((s + 1)) is non empty V11() real ext-real positive non negative set
K37(1,K39((s + 1))) is non empty V11() real ext-real positive non negative set
1 / (r + 1) is non empty V11() real ext-real positive non negative V160() Element of RAT
K39((r + 1)) is non empty V11() real ext-real positive non negative set
K37(1,K39((r + 1))) is non empty V11() real ext-real positive non negative set
X . s is V11() real ext-real Element of REAL
(X . s) - 0 is V11() real ext-real Element of REAL
K38(0) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued V49() V50() V53() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V134() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V167() Cardinal-yielding countable bounded_below bounded_above real-bounded V251() set
K36((X . s),K38(0)) is V11() real ext-real set
|.((X . s) - 0).| is V11() real ext-real Element of REAL
lim X is V11() real ext-real Element of REAL
m is non empty Relation-like non-empty NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))
F /* m is non empty Relation-like NAT -defined the carrier of G -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of G))
K7(NAT, the carrier of G) is non trivial Relation-like V49() set
K6(K7(NAT, the carrier of G)) is non trivial V49() set
m " is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(m ") (#) (F /* m) is non empty Relation-like NAT -defined the carrier of G -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of G))
lim ((m ") (#) (F /* m)) is Element of the carrier of G
0. G is V68(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
((m ") (#) (F /* m)) . i is Element of the carrier of G
(((m ") (#) (F /* m)) . i) - (0. G) is Element of the carrier of G
- (0. G) is Element of the carrier of G
(((m ") (#) (F /* m)) . i) + (- (0. G)) is Element of the carrier of G
the addF of G is Relation-like K7( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like total quasi_total Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is Relation-like set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is Relation-like set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is set
K462( the carrier of G, the addF of G,(((m ") (#) (F /* m)) . i),(- (0. G))) is Element of the carrier of G
||.((((m ") (#) (F /* m)) . i) - (0. G)).|| is V11() real ext-real non negative Element of REAL
the normF of G is non empty Relation-like the carrier of G -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of G,REAL))
K7( the carrier of G,REAL) is non trivial Relation-like complex-valued ext-real-valued real-valued V49() set
K6(K7( the carrier of G,REAL)) is non trivial V49() set
the normF of G . ((((m ") (#) (F /* m)) . i) - (0. G)) is V11() real ext-real Element of REAL
m . i is V11() real ext-real Element of REAL
F /. (m . i) is Element of the carrier of G
F . (m . i) is Element of the carrier of G
(m . i) " is V11() real ext-real Element of REAL
((m . i) ") * (F /. (m . i)) is Element of the carrier of G
the Mult of G is Relation-like K7(REAL, the carrier of G) -defined the carrier of G -valued Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of G), the carrier of G))
K7(K7(REAL, the carrier of G), the carrier of G) is non trivial Relation-like V49() set
K6(K7(K7(REAL, the carrier of G), the carrier of G)) is non trivial V49() set
K458( the Mult of G,((m . i) "),(F /. (m . i))) is set
||.(((m . i) ") * (F /. (m . i))).|| is V11() real ext-real non negative Element of REAL
the normF of G . (((m . i) ") * (F /. (m . i))) is V11() real ext-real Element of REAL
abs ((m . i) ") is V11() real ext-real Element of REAL
||.(F /. (m . i)).|| is V11() real ext-real non negative Element of REAL
the normF of G . (F /. (m . i)) is V11() real ext-real Element of REAL
(abs ((m . i) ")) * ||.(F /. (m . i)).|| is V11() real ext-real Element of REAL
|.(m . i).| is V11() real ext-real Element of REAL
|.(m . i).| " is V11() real ext-real Element of REAL
(|.(m . i).| ") * ||.(F /. (m . i)).|| is V11() real ext-real Element of REAL
rng m is non empty complex-membered ext-real-membered real-membered Element of K6(REAL)
||.(((m ") (#) (F /* m)) . i).|| is V11() real ext-real non negative Element of REAL
the normF of G . (((m ") (#) (F /* m)) . i) is V11() real ext-real Element of REAL
(F /* m) . i is Element of the carrier of G
(m ") . i is V11() real ext-real Element of REAL
((m ") . i) * ((F /* m) . i) is Element of the carrier of G
K458( the Mult of G,((m ") . i),((F /* m) . i)) is set
||.(((m ") . i) * ((F /* m) . i)).|| is V11() real ext-real non negative Element of REAL
the normF of G . (((m ") . i) * ((F /* m) . i)) is V11() real ext-real Element of REAL
((m . i) ") * ((F /* m) . i) is Element of the carrier of G
K458( the Mult of G,((m . i) "),((F /* m) . i)) is set
||.(((m . i) ") * ((F /* m) . i)).|| is V11() real ext-real non negative Element of REAL
the normF of G . (((m . i) ") * ((F /* m) . i)) is V11() real ext-real Element of REAL
i0 is V11() real ext-real Element of REAL
f is non empty Relation-like non-empty NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))
lim f is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued V49() V50() V53() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V134() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V167() Cardinal-yielding countable bounded_below bounded_above real-bounded V251() Element of REAL
X is V11() real ext-real Element of REAL
m is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
i0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
F /* f is non empty Relation-like NAT -defined the carrier of G -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of G))
f " is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
(f ") (#) (F /* f) is non empty Relation-like NAT -defined the carrier of G -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of G))
rng f is non empty complex-membered ext-real-membered real-membered Element of K6(REAL)
y0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
((f ") (#) (F /* f)) . y0 is Element of the carrier of G
(((f ") (#) (F /* f)) . y0) - (0. G) is Element of the carrier of G
(((f ") (#) (F /* f)) . y0) + (- (0. G)) is Element of the carrier of G
K462( the carrier of G, the addF of G,(((f ") (#) (F /* f)) . y0),(- (0. G))) is Element of the carrier of G
||.((((f ") (#) (F /* f)) . y0) - (0. G)).|| is V11() real ext-real non negative Element of REAL
the normF of G . ((((f ") (#) (F /* f)) . y0) - (0. G)) is V11() real ext-real Element of REAL
f . y0 is V11() real ext-real Element of REAL
(f . y0) - 0 is V11() real ext-real Element of REAL
K36((f . y0),K38(0)) is V11() real ext-real set
|.((f . y0) - 0).| is V11() real ext-real Element of REAL
|.(f . y0).| is V11() real ext-real Element of REAL
|.(f . y0).| " is V11() real ext-real Element of REAL
F /. (f . y0) is Element of the carrier of G
F . (f . y0) is Element of the carrier of G
||.(F /. (f . y0)).|| is V11() real ext-real non negative Element of REAL
the normF of G . (F /. (f . y0)) is V11() real ext-real Element of REAL
(|.(f . y0).| ") * ||.(F /. (f . y0)).|| is V11() real ext-real Element of REAL
(f . y0) " is V11() real ext-real Element of REAL
abs ((f . y0) ") is V11() real ext-real Element of REAL
(abs ((f . y0) ")) * ||.(F /. (f . y0)).|| is V11() real ext-real Element of REAL
((f . y0) ") * (F /. (f . y0)) is Element of the carrier of G
K458( the Mult of G,((f . y0) "),(F /. (f . y0))) is set
||.(((f . y0) ") * (F /. (f . y0))).|| is V11() real ext-real non negative Element of REAL
the normF of G . (((f . y0) ") * (F /. (f . y0))) is V11() real ext-real Element of REAL
(F /* f) . y0 is Element of the carrier of G
((f . y0) ") * ((F /* f) . y0) is Element of the carrier of G
K458( the Mult of G,((f . y0) "),((F /* f) . y0)) is set
||.(((f . y0) ") * ((F /* f) . y0)).|| is V11() real ext-real non negative Element of REAL
the normF of G . (((f . y0) ") * ((F /* f) . y0)) is V11() real ext-real Element of REAL
(f ") . y0 is V11() real ext-real Element of REAL
((f ") . y0) * ((F /* f) . y0) is Element of the carrier of G
K458( the Mult of G,((f ") . y0),((F /* f) . y0)) is set
||.(((f ") . y0) * ((F /* f) . y0)).|| is V11() real ext-real non negative Element of REAL
the normF of G . (((f ") . y0) * ((F /* f) . y0)) is V11() real ext-real Element of REAL
||.(((f ") (#) (F /* f)) . y0).|| is V11() real ext-real non negative Element of REAL
the normF of G . (((f ") (#) (F /* f)) . y0) is V11() real ext-real Element of REAL
lim ((f ") (#) (F /* f)) is Element of the carrier of G
f is V11() real ext-real Element of REAL
X is V11() real ext-real Element of REAL
G is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
the carrier of G is non empty non trivial set
K7(REAL, the carrier of G) is non trivial Relation-like V49() set
K6(K7(REAL, the carrier of G)) is non trivial V49() set
0. G is V68(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
F is Relation-like REAL -defined the carrier of G -valued Function-like RestFunc-like Element of K6(K7(REAL, the carrier of G))
F /. 0 is Element of the carrier of G
f is V11() real ext-real Element of REAL
X is V11() real ext-real Element of REAL
m is V11() real ext-real Element of REAL
|.m.| is V11() real ext-real Element of REAL
|.m.| " is V11() real ext-real Element of REAL
F /. m is Element of the carrier of G
||.(F /. m).|| is V11() real ext-real non negative Element of REAL
the normF of G is non empty Relation-like the carrier of G -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of G,REAL))
K7( the carrier of G,REAL) is non trivial Relation-like complex-valued ext-real-valued real-valued V49() set
K6(K7( the carrier of G,REAL)) is non trivial V49() set
the normF of G . (F /. m) is V11() real ext-real Element of REAL
(|.m.| ") * ||.(F /. m).|| is V11() real ext-real Element of REAL
|.m.| * ((|.m.| ") * ||.(F /. m).||) is V11() real ext-real Element of REAL
|.m.| * f is V11() real ext-real Element of REAL
|.m.| * (|.m.| ") is V11() real ext-real Element of REAL
(|.m.| * (|.m.| ")) * ||.(F /. m).|| is V11() real ext-real Element of REAL
f * |.m.| is V11() real ext-real Element of REAL
1 * ||.(F /. m).|| is V11() real ext-real non negative Element of REAL
i is V11() real ext-real Element of REAL
i * |.m.| is V11() real ext-real Element of REAL
f * |.m.| is V11() real ext-real Element of REAL
F /. m is Element of the carrier of G
||.(F /. m).|| is V11() real ext-real non negative Element of REAL
the normF of G is non empty Relation-like the carrier of G -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of G,REAL))
K7( the carrier of G,REAL) is non trivial Relation-like complex-valued ext-real-valued real-valued V49() set
K6(K7( the carrier of G,REAL)) is non trivial V49() set
the normF of G . (F /. m) is V11() real ext-real Element of REAL
m is V11() real ext-real Element of REAL
|.m.| is V11() real ext-real Element of REAL
F /. m is Element of the carrier of G
||.(F /. m).|| is V11() real ext-real non negative Element of REAL
the normF of G is non empty Relation-like the carrier of G -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of G,REAL))
K7( the carrier of G,REAL) is non trivial Relation-like complex-valued ext-real-valued real-valued V49() set
K6(K7( the carrier of G,REAL)) is non trivial V49() set
the normF of G . (F /. m) is V11() real ext-real Element of REAL
f * |.m.| is V11() real ext-real Element of REAL
G is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
the carrier of G is non empty non trivial set
K7(REAL, the carrier of G) is non trivial Relation-like V49() set
K6(K7(REAL, the carrier of G)) is non trivial V49() set
F is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
the carrier of F is non empty non trivial set
K7( the carrier of G, the carrier of F) is Relation-like set
K6(K7( the carrier of G, the carrier of F)) is set
K7(REAL, the carrier of F) is non trivial Relation-like V49() set
K6(K7(REAL, the carrier of F)) is non trivial V49() set
f is Relation-like REAL -defined the carrier of G -valued Function-like RestFunc-like Element of K6(K7(REAL, the carrier of G))
X is non empty Relation-like the carrier of G -defined the carrier of F -valued Function-like total quasi_total V153(G,F) V154(G,F) Lipschitzian Element of K6(K7( the carrier of G, the carrier of F))
X * f is Relation-like REAL -defined the carrier of F -valued Function-like Element of K6(K7(REAL, the carrier of F))
m is V11() real ext-real Element of REAL
dom X is non empty Element of K6( the carrier of G)
K6( the carrier of G) is set
rng f is Element of K6( the carrier of G)
dom f is complex-membered ext-real-membered real-membered Element of K6(REAL)
i is V11() real ext-real Element of REAL
i / 2 is V11() real ext-real Element of REAL
K39(2) is non empty V11() real ext-real positive non negative set
K37(i,K39(2)) is V11() real ext-real set
1 + m is V11() real ext-real Element of REAL
(i / 2) / (1 + m) is V11() real ext-real Element of REAL
K39((1 + m)) is V11() real ext-real set
K37((i / 2),K39((1 + m))) is V11() real ext-real set
y0 is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
|.r.| is V11() real ext-real Element of REAL
|.r.| " is V11() real ext-real Element of REAL
f /. r is Element of the carrier of G
||.(f /. r).|| is V11() real ext-real non negative Element of REAL
the normF of G is non empty Relation-like the carrier of G -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of G,REAL))
K7( the carrier of G,REAL) is non trivial Relation-like complex-valued ext-real-valued real-valued V49() set
K6(K7( the carrier of G,REAL)) is non trivial V49() set
the normF of G . (f /. r) is V11() real ext-real Element of REAL
(|.r.| ") * ||.(f /. r).|| is V11() real ext-real Element of REAL
m + 1 is V11() real ext-real Element of REAL
(m + 1) * ((|.r.| ") * ||.(f /. r).||) is V11() real ext-real Element of REAL
(m + 1) * ((i / 2) / (1 + m)) is V11() real ext-real Element of REAL
y1 is V11() real ext-real Element of REAL
y1 + m is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
s + m is V11() real ext-real Element of REAL
m * ||.(f /. r).|| is V11() real ext-real Element of REAL
(m + 1) * ||.(f /. r).|| is V11() real ext-real Element of REAL
X . (f /. r) is Element of the carrier of F
||.(X . (f /. r)).|| is V11() real ext-real non negative Element of REAL
the normF of F is non empty Relation-like the carrier of F -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of F,REAL))
K7( the carrier of F,REAL) is non trivial Relation-like complex-valued ext-real-valued real-valued V49() set
K6(K7( the carrier of F,REAL)) is non trivial V49() set
the normF of F . (X . (f /. r)) is V11() real ext-real Element of REAL
(|.r.| ") * ||.(X . (f /. r)).|| is V11() real ext-real Element of REAL
(|.r.| ") * ((m + 1) * ||.(f /. r).||) is V11() real ext-real Element of REAL
X /. (f /. r) is Element of the carrier of F
(X * f) /. r is Element of the carrier of F
||.((X * f) /. r).|| is V11() real ext-real non negative Element of REAL
the normF of F . ((X * f) /. r) is V11() real ext-real Element of REAL
(|.r.| ") * ||.((X * f) /. r).|| is V11() real ext-real Element of REAL
G is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
the carrier of G is non empty non trivial set
K7(REAL, the carrier of G) is non trivial Relation-like V49() set
K6(K7(REAL, the carrier of G)) is non trivial V49() set
0. G is V68(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
F is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
the carrier of F is non empty non trivial set
K7( the carrier of G, the carrier of F) is Relation-like set
K6(K7( the carrier of G, the carrier of F)) is set
0. F is V68(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
K7(REAL, the carrier of F) is non trivial Relation-like V49() set
K6(K7(REAL, the carrier of F)) is non trivial V49() set
f is Relation-like REAL -defined the carrier of G -valued Function-like RestFunc-like Element of K6(K7(REAL, the carrier of G))
f /. 0 is Element of the carrier of G
X is V11() real ext-real Element of REAL
m is Relation-like the carrier of G -defined the carrier of F -valued Function-like RestFunc-like Element of K6(K7( the carrier of G, the carrier of F))
m /. (0. G) is Element of the carrier of F
i is non empty Relation-like REAL -defined the carrier of G -valued Function-like total quasi_total linear Element of K6(K7(REAL, the carrier of G))
i + f is Relation-like REAL -defined the carrier of G -valued Function-like Element of K6(K7(REAL, the carrier of G))
m * (i + f) is Relation-like REAL -defined the carrier of F -valued Function-like Element of K6(K7(REAL, the carrier of F))
i0 is Element of the carrier of G
||.i0.|| is V11() real ext-real non negative Element of REAL
the normF of G is non empty Relation-like the carrier of G -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of G,REAL))
K7( the carrier of G,REAL) is non trivial Relation-like complex-valued ext-real-valued real-valued V49() set
K6(K7( the carrier of G,REAL)) is non trivial V49() set
the normF of G . i0 is V11() real ext-real Element of REAL
dom m is Element of K6( the carrier of G)
K6( the carrier of G) is set
rng (i + f) is Element of K6( the carrier of G)
dom (i + f) is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (m * (i + f)) is complex-membered ext-real-membered real-membered Element of K6(REAL)
r is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
K39(2) is non empty V11() real ext-real positive non negative set
K37(r,K39(2)) is V11() real ext-real set
y0 is V11() real ext-real Element of REAL
1 + y0 is V11() real ext-real Element of REAL
(r / 2) / (1 + y0) is V11() real ext-real Element of REAL
K39((1 + y0)) is V11() real ext-real set
K37((r / 2),K39((1 + y0))) is V11() real ext-real set
y1 is V11() real ext-real Element of REAL
y1 / (1 + y0) is V11() real ext-real Element of REAL
K37(y1,K39((1 + y0))) is V11() real ext-real set
min (X,(y1 / (1 + y0))) is V11() real ext-real Element of REAL
a is V11() real ext-real Element of REAL
|.a.| is V11() real ext-real Element of REAL
f /. a is Element of the carrier of G
||.(f /. a).|| is V11() real ext-real non negative Element of REAL
the normF of G . (f /. a) is V11() real ext-real Element of REAL
1 * |.a.| is V11() real ext-real Element of REAL
i . a is Element of the carrier of G
a * i0 is Element of the carrier of G
the Mult of G is Relation-like K7(REAL, the carrier of G) -defined the carrier of G -valued Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of G), the carrier of G))
K7(K7(REAL, the carrier of G), the carrier of G) is non trivial Relation-like V49() set
K6(K7(K7(REAL, the carrier of G), the carrier of G)) is non trivial V49() set
K458( the Mult of G,a,i0) is set
||.(i . a).|| is V11() real ext-real non negative Element of REAL
the normF of G . (i . a) is V11() real ext-real Element of REAL
y0 * |.a.| is V11() real ext-real Element of REAL
||.(i . a).|| - (y0 * |.a.|) is V11() real ext-real Element of REAL
K38((y0 * |.a.|)) is V11() real ext-real set
K36(||.(i . a).||,K38((y0 * |.a.|))) is V11() real ext-real set
(||.(i . a).|| - (y0 * |.a.|)) + (y0 * |.a.|) is V11() real ext-real Element of REAL
t is V11() real ext-real Element of REAL
t + (y0 * |.a.|) is V11() real ext-real Element of REAL
(i . a) + (f /. a) is Element of the carrier of G
the addF of G is Relation-like K7( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like total quasi_total Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is Relation-like set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is Relation-like set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is set
K462( the carrier of G, the addF of G,(i . a),(f /. a)) is Element of the carrier of G
||.((i . a) + (f /. a)).|| is V11() real ext-real non negative Element of REAL
the normF of G . ((i . a) + (f /. a)) is V11() real ext-real Element of REAL
||.(i . a).|| + ||.(f /. a).|| is V11() real ext-real non negative Element of REAL
(y0 * |.a.|) + (1 * |.a.|) is V11() real ext-real Element of REAL
y0 + 1 is V11() real ext-real Element of REAL
(y0 + 1) * |.a.| is V11() real ext-real Element of REAL
((r / 2) / (1 + y0)) * ||.((i . a) + (f /. a)).|| is V11() real ext-real Element of REAL
((r / 2) / (1 + y0)) * ((y0 + 1) * |.a.|) is V11() real ext-real Element of REAL
(y0 + 1) * (y1 / (1 + y0)) is V11() real ext-real Element of REAL
m /. ((i . a) + (f /. a)) is Element of the carrier of F
||.(m /. ((i . a) + (f /. a))).|| is V11() real ext-real non negative Element of REAL
the normF of F is non empty Relation-like the carrier of F -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of F,REAL))
K7( the carrier of F,REAL) is non trivial Relation-like complex-valued ext-real-valued real-valued V49() set
K6(K7( the carrier of F,REAL)) is non trivial V49() set
the normF of F . (m /. ((i . a) + (f /. a))) is V11() real ext-real Element of REAL
i /. a is Element of the carrier of G
(i /. a) + (f /. a) is Element of the carrier of G
K462( the carrier of G, the addF of G,(i /. a),(f /. a)) is Element of the carrier of G
m /. ((i /. a) + (f /. a)) is Element of the carrier of F
(i + f) /. a is Element of the carrier of G
m /. ((i + f) /. a) is Element of the carrier of F
(m * (i + f)) /. a is Element of the carrier of F
|.a.| " is V11() real ext-real Element of REAL
||.((m * (i + f)) /. a).|| is V11() real ext-real non negative Element of REAL
the normF of F . ((m * (i + f)) /. a) is V11() real ext-real Element of REAL
(|.a.| ") * ||.((m * (i + f)) /. a).|| is V11() real ext-real Element of REAL
((r / 2) / (1 + y0)) * (y0 + 1) is V11() real ext-real Element of REAL
(((r / 2) / (1 + y0)) * (y0 + 1)) * |.a.| is V11() real ext-real Element of REAL
(|.a.| ") * ((((r / 2) / (1 + y0)) * (y0 + 1)) * |.a.|) is V11() real ext-real Element of REAL
|.a.| * (|.a.| ") is V11() real ext-real Element of REAL
(|.a.| * (|.a.| ")) * ((r / 2) / (1 + y0)) is V11() real ext-real Element of REAL
((|.a.| * (|.a.| ")) * ((r / 2) / (1 + y0))) * (y0 + 1) is V11() real ext-real Element of REAL
1 * ((r / 2) / (1 + y0)) is V11() real ext-real Element of REAL
(1 * ((r / 2) / (1 + y0))) * (y0 + 1) is V11() real ext-real Element of REAL
G is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
the carrier of G is non empty non trivial set
K7(REAL, the carrier of G) is non trivial Relation-like V49() set
K6(K7(REAL, the carrier of G)) is non trivial V49() set
0. G is V68(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
F is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
the carrier of F is non empty non trivial set
K7( the carrier of G, the carrier of F) is Relation-like set
K6(K7( the carrier of G, the carrier of F)) is set
0. F is V68(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
K7(REAL, the carrier of F) is non trivial Relation-like V49() set
K6(K7(REAL, the carrier of F)) is non trivial V49() set
f is Relation-like REAL -defined the carrier of G -valued Function-like RestFunc-like Element of K6(K7(REAL, the carrier of G))
f /. 0 is Element of the carrier of G
X is Relation-like the carrier of G -defined the carrier of F -valued Function-like RestFunc-like Element of K6(K7( the carrier of G, the carrier of F))
X /. (0. G) is Element of the carrier of F
m is non empty Relation-like REAL -defined the carrier of G -valued Function-like total quasi_total linear Element of K6(K7(REAL, the carrier of G))
m + f is Relation-like REAL -defined the carrier of G -valued Function-like Element of K6(K7(REAL, the carrier of G))
X * (m + f) is Relation-like REAL -defined the carrier of F -valued Function-like Element of K6(K7(REAL, the carrier of F))
i is non empty Relation-like the carrier of G -defined the carrier of F -valued Function-like total quasi_total V153(G,F) V154(G,F) Lipschitzian Element of K6(K7( the carrier of G, the carrier of F))
i * f is Relation-like REAL -defined the carrier of F -valued Function-like Element of K6(K7(REAL, the carrier of F))
(i * f) + (X * (m + f)) is Relation-like REAL -defined the carrier of F -valued Function-like Element of K6(K7(REAL, the carrier of F))
G is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
the carrier of G is non empty non trivial set
K7(REAL, the carrier of G) is non trivial Relation-like V49() set
K6(K7(REAL, the carrier of G)) is non trivial V49() set
F is non empty non trivial right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
the carrier of F is non empty non trivial set
K7( the carrier of G, the carrier of F) is Relation-like set
K6(K7( the carrier of G, the carrier of F)) is set
f is V11() real ext-real Element of REAL
X is Relation-like REAL -defined the carrier of G -valued Function-like Element of K6(K7(REAL, the carrier of G))
X /. f is Element of the carrier of G
diff (X,f) is Element of the carrier of G
dom X is complex-membered ext-real-membered real-membered Element of K6(REAL)
m is complex-membered ext-real-membered real-membered open Neighbourhood of f
i is Relation-like the carrier of G -defined the carrier of F -valued Function-like Element of K6(K7( the carrier of G, the carrier of F))
i * X is Relation-like REAL -defined the carrier of F -valued Function-like Element of K6(K7(REAL, the carrier of F))
K7(REAL, the carrier of F) is non trivial Relation-like V49() set
K6(K7(REAL, the carrier of F)) is non trivial V49() set
diff ((i * X),f) is Element of the carrier of F
diff (i,(X /. f)) is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (G,F))
R_NormSpace_of_BoundedLinearOperators (G,F) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
BoundedLinearOperators (G,F) is non empty Element of K6( the carrier of (R_VectorSpace_of_LinearOperators (G,F)))
R_VectorSpace_of_LinearOperators (G,F) is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital constituted-Functions RLSStruct
LinearOperators (G,F) is non empty functional Element of K6( the carrier of K266( the carrier of G,F))
K266( the carrier of G,F) is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital constituted-Functions RLSStruct
Funcs ( the carrier of G, the carrier of F) is non empty functional FUNCTION_DOMAIN of the carrier of G, the carrier of F
FuncZero ( the carrier of G,F) is Relation-like the carrier of G -defined the carrier of F -valued Function-like total quasi_total Element of Funcs ( the carrier of G, the carrier of F)
0. F is V68(F) Element of the carrier of F
the ZeroF of F is Element of the carrier of F
the carrier of G --> (0. F) is non empty Relation-like the carrier of G -defined the carrier of F -valued Function-like constant total quasi_total Element of K6(K7( the carrier of G, the carrier of F))
FuncAdd ( the carrier of G,F) is Relation-like K7((Funcs ( the carrier of G, the carrier of F)),(Funcs ( the carrier of G, the carrier of F))) -defined Funcs ( the carrier of G, the carrier of F) -valued Function-like total quasi_total Function-yielding V134() Element of K6(K7(K7((Funcs ( the carrier of G, the carrier of F)),(Funcs ( the carrier of G, the carrier of F))),(Funcs ( the carrier of G, the carrier of F))))
K7((Funcs ( the carrier of G, the carrier of F)),(Funcs ( the carrier of G, the carrier of F))) is Relation-like set
K7(K7((Funcs ( the carrier of G, the carrier of F)),(Funcs ( the carrier of G, the carrier of F))),(Funcs ( the carrier of G, the carrier of F))) is Relation-like set
K6(K7(K7((Funcs ( the carrier of G, the carrier of F)),(Funcs ( the carrier of G, the carrier of F))),(Funcs ( the carrier of G, the carrier of F)))) is set
FuncExtMult ( the carrier of G,F) is Relation-like K7(REAL,(Funcs ( the carrier of G, the carrier of F))) -defined Funcs ( the carrier of G, the carrier of F) -valued Function-like total quasi_total Function-yielding V134() Element of K6(K7(K7(REAL,(Funcs ( the carrier of G, the carrier of F))),(Funcs ( the carrier of G, the carrier of F))))
K7(REAL,(Funcs ( the carrier of G, the carrier of F))) is non trivial Relation-like V49() set
K7(K7(REAL,(Funcs ( the carrier of G, the carrier of F))),(Funcs ( the carrier of G, the carrier of F))) is non trivial Relation-like V49() set
K6(K7(K7(REAL,(Funcs ( the carrier of G, the carrier of F))),(Funcs ( the carrier of G, the carrier of F)))) is non trivial V49() set
RLSStruct(# (Funcs ( the carrier of G, the carrier of F)),(FuncZero ( the carrier of G,F)),(FuncAdd ( the carrier of G,F)),(FuncExtMult ( the carrier of G,F)) #) is strict RLSStruct
the carrier of K266( the carrier of G,F) is non empty set
K6( the carrier of K266( the carrier of G,F)) is set
K215(K266( the carrier of G,F),(LinearOperators (G,F))) is Relation-like Function-like Element of LinearOperators (G,F)
K213(K266( the carrier of G,F),(LinearOperators (G,F))) is Relation-like K7((LinearOperators (G,F)),(LinearOperators (G,F))) -defined LinearOperators (G,F) -valued Function-like total quasi_total Function-yielding V134() Element of K6(K7(K7((LinearOperators (G,F)),(LinearOperators (G,F))),(LinearOperators (G,F))))
K7((LinearOperators (G,F)),(LinearOperators (G,F))) is Relation-like set
K7(K7((LinearOperators (G,F)),(LinearOperators (G,F))),(LinearOperators (G,F))) is Relation-like set
K6(K7(K7((LinearOperators (G,F)),(LinearOperators (G,F))),(LinearOperators (G,F)))) is set
K214(K266( the carrier of G,F),(LinearOperators (G,F))) is Relation-like K7(REAL,(LinearOperators (G,F))) -defined LinearOperators (G,F) -valued Function-like total quasi_total Function-yielding V134() Element of K6(K7(K7(REAL,(LinearOperators (G,F))),(LinearOperators (G,F))))
K7(REAL,(LinearOperators (G,F))) is non trivial Relation-like V49() set
K7(K7(REAL,(LinearOperators (G,F))),(LinearOperators (G,F))) is non trivial Relation-like V49() set
K6(K7(K7(REAL,(LinearOperators (G,F))),(LinearOperators (G,F)))) is non trivial V49() set
RLSStruct(# (LinearOperators (G,F)),K215(K266( the carrier of G,F),(LinearOperators (G,F))),K213(K266( the carrier of G,F),(LinearOperators (G,F))),K214(K266( the carrier of G,F),(LinearOperators (G,F))) #) is right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of (R_VectorSpace_of_LinearOperators (G,F)) is non empty set
K6( the carrier of (R_VectorSpace_of_LinearOperators (G,F))) is set
K215((R_VectorSpace_of_LinearOperators (G,F)),(BoundedLinearOperators (G,F))) is Element of BoundedLinearOperators (G,F)
K213((R_VectorSpace_of_LinearOperators (G,F)),(BoundedLinearOperators (G,F))) is Relation-like K7((BoundedLinearOperators (G,F)),(BoundedLinearOperators (G,F))) -defined BoundedLinearOperators (G,F) -valued Function-like total quasi_total Element of K6(K7(K7((BoundedLinearOperators (G,F)),(BoundedLinearOperators (G,F))),(BoundedLinearOperators (G,F))))
K7((BoundedLinearOperators (G,F)),(BoundedLinearOperators (G,F))) is Relation-like set
K7(K7((BoundedLinearOperators (G,F)),(BoundedLinearOperators (G,F))),(BoundedLinearOperators (G,F))) is Relation-like set
K6(K7(K7((BoundedLinearOperators (G,F)),(BoundedLinearOperators (G,F))),(BoundedLinearOperators (G,F)))) is set
K214((R_VectorSpace_of_LinearOperators (G,F)),(BoundedLinearOperators (G,F))) is Relation-like K7(REAL,(BoundedLinearOperators (G,F))) -defined BoundedLinearOperators (G,F) -valued Function-like total quasi_total Element of K6(K7(K7(REAL,(BoundedLinearOperators (G,F))),(BoundedLinearOperators (G,F))))
K7(REAL,(BoundedLinearOperators (G,F))) is non trivial Relation-like V49() set
K7(K7(REAL,(BoundedLinearOperators (G,F))),(BoundedLinearOperators (G,F))) is non trivial Relation-like V49() set
K6(K7(K7(REAL,(BoundedLinearOperators (G,F))),(BoundedLinearOperators (G,F)))) is non trivial V49() set
BoundedLinearOperatorsNorm (G,F) is non empty Relation-like BoundedLinearOperators (G,F) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((BoundedLinearOperators (G,F)),REAL))
K7((BoundedLinearOperators (G,F)),REAL) is non trivial Relation-like complex-valued ext-real-valued real-valued V49() set
K6(K7((BoundedLinearOperators (G,F)),REAL)) is non trivial V49() set
NORMSTR(# (BoundedLinearOperators (G,F)),K215((R_VectorSpace_of_LinearOperators (G,F)),(BoundedLinearOperators (G,F))),K213((R_VectorSpace_of_LinearOperators (G,F)),(BoundedLinearOperators (G,F))),K214((R_VectorSpace_of_LinearOperators (G,F)),(BoundedLinearOperators (G,F))),(BoundedLinearOperatorsNorm (G,F)) #) is strict NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators (G,F)) is non empty set
(diff (i,(X /. f))) . (diff (X,f)) is Element of the carrier of F
dom i is Element of K6( the carrier of G)
K6( the carrier of G) is set
0. G is V68(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
i /. (X /. f) is Element of the carrier of F
i0 is Neighbourhood of X /. f
y0 is Relation-like the carrier of G -defined the carrier of F -valued Function-like RestFunc-like Element of K6(K7( the carrier of G, the carrier of F))
y0 /. (0. G) is Element of the carrier of F
y0 is Relation-like the carrier of G -defined the carrier of F -valued Function-like RestFunc-like Element of K6(K7( the carrier of G, the carrier of F))
y0 /. (0. G) is Element of the carrier of F
s is non empty Relation-like REAL -defined the carrier of G -valued Function-like total quasi_total linear Element of K6(K7(REAL, the carrier of G))
s . 1 is Element of the carrier of G
y1 is Relation-like REAL -defined the carrier of G -valued Function-like RestFunc-like Element of K6(K7(REAL, the carrier of G))
s is non empty Relation-like REAL -defined the carrier of G -valued Function-like total quasi_total linear Element of K6(K7(REAL, the carrier of G))
s . 1 is Element of the carrier of G
y1 is Relation-like REAL -defined the carrier of G -valued Function-like RestFunc-like Element of K6(K7(REAL, the carrier of G))
PP is Element of the carrier of G
(X /. f) - (X /. f) is Element of the carrier of G
- (X /. f) is Element of the carrier of G
(X /. f) + (- (X /. f)) is Element of the carrier of G
the addF of G is Relation-like K7( the carrier of G, the carrier of G) -defined the carrier of G -valued Function-like total quasi_total Element of K6(K7(K7( the carrier of G, the carrier of G), the carrier of G))
K7( the carrier of G, the carrier of G) is Relation-like set
K7(K7( the carrier of G, the carrier of G), the carrier of G) is Relation-like set
K6(K7(K7( the carrier of G, the carrier of G), the carrier of G)) is set
K462( the carrier of G, the addF of G,(X /. f),(- (X /. f))) is Element of the carrier of G
f - f is V11() real ext-real Element of REAL
K38(f) is V11() real ext-real set
K36(f,K38(f)) is V11() real ext-real set
s . (f - f) is Element of the carrier of G
y1 /. (f - f) is Element of the carrier of G
(s . (f - f)) + (y1 /. (f - f)) is Element of the carrier of G
K462( the carrier of G, the addF of G,(s . (f - f)),(y1 /. (f - f))) is Element of the carrier of G
s . 0 is Element of the carrier of G
y1 /. 0 is Element of the carrier of G
(s . 0) + (y1 /. 0) is Element of the carrier of G
K462( the carrier of G, the addF of G,(s . 0),(y1 /. 0)) is Element of the carrier of G
DD is V11() real ext-real Element of REAL
DD * PP is Element of the carrier of G
the Mult of G is Relation-like K7(REAL, the carrier of G) -defined the carrier of G -valued Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of G), the carrier of G))
K7(K7(REAL, the carrier of G), the carrier of G) is non trivial Relation-like V49() set
K6(K7(K7(REAL, the carrier of G), the carrier of G)) is non trivial V49() set
K458( the Mult of G,DD,PP) is set
(DD * PP) + (y1 /. 0) is Element of the carrier of G
K462( the carrier of G, the addF of G,(DD * PP),(y1 /. 0)) is Element of the carrier of G
(0. G) + (y1 /. 0) is Element of the carrier of G
K462( the carrier of G, the addF of G,(0. G),(y1 /. 0)) is Element of the carrier of G
r is non empty Relation-like the carrier of G -defined the carrier of F -valued Function-like total quasi_total V153(G,F) V154(G,F) Lipschitzian Element of K6(K7( the carrier of G, the carrier of F))
r * y1 is Relation-like REAL -defined the carrier of F -valued Function-like Element of K6(K7(REAL, the carrier of F))
s + y1 is Relation-like REAL -defined the carrier of G -valued Function-like Element of K6(K7(REAL, the carrier of G))
y0 * (s + y1) is Relation-like REAL -defined the carrier of F -valued Function-like Element of K6(K7(REAL, the carrier of F))
(r * y1) + (y0 * (s + y1)) is Relation-like REAL -defined the carrier of F -valued Function-like Element of K6(K7(REAL, the carrier of F))
r * s is non empty Relation-like REAL -defined the carrier of F -valued Function-like total quasi_total Element of K6(K7(REAL, the carrier of F))
dom (r * s) is non empty complex-membered ext-real-membered real-membered Element of K6(REAL)
r . PP is Element of the carrier of F
tm is V11() real ext-real Element of REAL
s . tm is Element of the carrier of G
r . (s . tm) is Element of the carrier of F
tm * PP is Element of the carrier of G
K458( the Mult of G,tm,PP) is set
r . (tm * PP) is Element of the carrier of F
t is Element of the carrier of F
tm * t is Element of the carrier of F
the Mult of F is Relation-like K7(REAL, the carrier of F) -defined the carrier of F -valued Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of F), the carrier of F))
K7(K7(REAL, the carrier of F), the carrier of F) is non trivial Relation-like V49() set
K6(K7(K7(REAL, the carrier of F), the carrier of F)) is non trivial V49() set
K458( the Mult of F,tm,t) is set
(r * s) . tm is Element of the carrier of F
Sw1 is complex-membered ext-real-membered real-membered open Neighbourhood of f
X .: Sw1 is Element of K6( the carrier of G)
w2 is complex-membered ext-real-membered real-membered open Neighbourhood of f
ys is set
rm is V11() real ext-real Element of REAL
X . rm is set
dom (i * X) is complex-membered ext-real-membered real-membered Element of K6(REAL)
ys is V11() real ext-real Element of REAL
X /. ys is Element of the carrier of G
(X /. ys) - (X /. f) is Element of the carrier of G
(X /. ys) + (- (X /. f)) is Element of the carrier of G
K462( the carrier of G, the addF of G,(X /. ys),(- (X /. f))) is Element of the carrier of G
ys - f is V11() real ext-real Element of REAL
K36(ys,K38(f)) is V11() real ext-real set
s . (ys - f) is Element of the carrier of G
y1 /. (ys - f) is Element of the carrier of G
(s . (ys - f)) + (y1 /. (ys - f)) is Element of the carrier of G
K462( the carrier of G, the addF of G,(s . (ys - f)),(y1 /. (ys - f))) is Element of the carrier of G
X . ys is set
dom y1 is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom r is non empty Element of K6( the carrier of G)
rng y1 is Element of K6( the carrier of G)
dom (r * y1) is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom (s + y1) is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom y0 is Element of K6( the carrier of G)
rng (s + y1) is Element of K6( the carrier of G)
dom (y0 * (s + y1)) is complex-membered ext-real-membered real-membered Element of K6(REAL)
dom ((r * y1) + (y0 * (s + y1))) is complex-membered ext-real-membered real-membered Element of K6(REAL)
REAL /\ REAL is complex-membered ext-real-membered real-membered V251() set
r . (y1 /. (ys - f)) is Element of the carrier of F
r /. (y1 /. (ys - f)) is Element of the carrier of F
(r * y1) /. (ys - f) is Element of the carrier of F
y0 /. ((s . (ys - f)) + (y1 /. (ys - f))) is Element of the carrier of F
s /. (ys - f) is Element of the carrier of G
(s /. (ys - f)) + (y1 /. (ys - f)) is Element of the carrier of G
K462( the carrier of G, the addF of G,(s /. (ys - f)),(y1 /. (ys - f))) is Element of the carrier of G
y0 /. ((s /. (ys - f)) + (y1 /. (ys - f))) is Element of the carrier of F
(s + y1) /. (ys - f) is Element of the carrier of G
y0 /. ((s + y1) /. (ys - f)) is Element of the carrier of F
(y0 * (s + y1)) /. (ys - f) is Element of the carrier of F
(r * s) . (ys - f) is Element of the carrier of F
r . (s . (ys - f)) is Element of the carrier of F
(i * X) /. ys is Element of the carrier of F
(i * X) /. f is Element of the carrier of F
((i * X) /. ys) - ((i * X) /. f) is Element of the carrier of F
- ((i * X) /. f) is Element of the carrier of F
((i * X) /. ys) + (- ((i * X) /. f)) is Element of the carrier of F
the addF of F is Relation-like K7( the carrier of F, the carrier of F) -defined the carrier of F -valued Function-like total quasi_total Element of K6(K7(K7( the carrier of F, the carrier of F), the carrier of F))
K7( the carrier of F, the carrier of F) is Relation-like set
K7(K7( the carrier of F, the carrier of F), the carrier of F) is Relation-like set
K6(K7(K7( the carrier of F, the carrier of F), the carrier of F)) is set
K462( the carrier of F, the addF of F,((i * X) /. ys),(- ((i * X) /. f))) is Element of the carrier of F
i /. (X /. ys) is Element of the carrier of F
(i /. (X /. ys)) - ((i * X) /. f) is Element of the carrier of F
(i /. (X /. ys)) + (- ((i * X) /. f)) is Element of the carrier of F
K462( the carrier of F, the addF of F,(i /. (X /. ys)),(- ((i * X) /. f))) is Element of the carrier of F
(i /. (X /. ys)) - (i /. (X /. f)) is Element of the carrier of F
- (i /. (X /. f)) is Element of the carrier of F
(i /. (X /. ys)) + (- (i /. (X /. f))) is Element of the carrier of F
K462( the carrier of F, the addF of F,(i /. (X /. ys)),(- (i /. (X /. f)))) is Element of the carrier of F
(diff (i,(X /. f))) . ((X /. ys) - (X /. f)) is Element of the carrier of F
y0 /. ((X /. ys) - (X /. f)) is Element of the carrier of F
((diff (i,(X /. f))) . ((X /. ys) - (X /. f))) + (y0 /. ((X /. ys) - (X /. f))) is Element of the carrier of F
K462( the carrier of F, the addF of F,((diff (i,(X /. f))) . ((X /. ys) - (X /. f))),(y0 /. ((X /. ys) - (X /. f)))) is Element of the carrier of F
(r . (s . (ys - f))) + (r . (y1 /. (ys - f))) is Element of the carrier of F
K462( the carrier of F, the addF of F,(r . (s . (ys - f))),(r . (y1 /. (ys - f)))) is Element of the carrier of F
((r . (s . (ys - f))) + (r . (y1 /. (ys - f)))) + ((y0 * (s + y1)) /. (ys - f)) is Element of the carrier of F
K462( the carrier of F, the addF of F,((r . (s . (ys - f))) + (r . (y1 /. (ys - f)))),((y0 * (s + y1)) /. (ys - f))) is Element of the carrier of F
((r * y1) /. (ys - f)) + ((y0 * (s + y1)) /. (ys - f)) is Element of the carrier of F
K462( the carrier of F, the addF of F,((r * y1) /. (ys - f)),((y0 * (s + y1)) /. (ys - f))) is Element of the carrier of F
(r . (s . (ys - f))) + (((r * y1) /. (ys - f)) + ((y0 * (s + y1)) /. (ys - f))) is Element of the carrier of F
K462( the carrier of F, the addF of F,(r . (s . (ys - f))),(((r * y1) /. (ys - f)) + ((y0 * (s + y1)) /. (ys - f)))) is Element of the carrier of F
tm is non empty Relation-like REAL -defined the carrier of F -valued Function-like total quasi_total linear Element of K6(K7(REAL, the carrier of F))
tm . (ys - f) is Element of the carrier of F
a is Relation-like REAL -defined the carrier of F -valued Function-like RestFunc-like Element of K6(K7(REAL, the carrier of F))
a /. (ys - f) is Element of the carrier of F
(tm . (ys - f)) + (a /. (ys - f)) is Element of the carrier of F
K462( the carrier of F, the addF of F,(tm . (ys - f)),(a /. (ys - f))) is Element of the carrier of F
(r * s) . 1 is Element of the carrier of F
G is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like NORMSTR
the carrier of G is non empty set
F is Relation-like NAT -defined the carrier of G -valued Function-like V49() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G
len F is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
dom F is V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of K6(NAT)
Sum F is Element of the carrier of G
||.(Sum F).|| is V11() real ext-real non negative Element of REAL
the normF of G is non empty Relation-like the carrier of G -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of G,REAL))
K7( the carrier of G,REAL) is non trivial Relation-like complex-valued ext-real-valued real-valued V49() set
K6(K7( the carrier of G,REAL)) is non trivial V49() set
the normF of G . (Sum F) is V11() real ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V49() FinSequence-like FinSubsequence-like countable FinSequence of REAL
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
Sum f is V11() real ext-real Element of REAL
X is Relation-like NAT -defined the carrier of G -valued Function-like V49() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G
len X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
dom X is V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of K6(NAT)
Sum X is Element of the carrier of G
||.(Sum X).|| is V11() real ext-real non negative Element of REAL
the normF of G . (Sum X) is V11() real ext-real Element of REAL
m is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V49() FinSequence-like FinSubsequence-like countable FinSequence of REAL
len m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
Sum m is V11() real ext-real Element of REAL
K7(NAT, the carrier of G) is non trivial Relation-like V49() set
K6(K7(NAT, the carrier of G)) is non trivial V49() set
0. G is V68(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
i is non empty Relation-like NAT -defined the carrier of G -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of G))
i . (len X) is Element of the carrier of G
i . 0 is Element of the carrier of G
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
m is Relation-like NAT -defined the carrier of G -valued Function-like V49() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G
m | X is Relation-like NAT -defined the carrier of G -valued Function-like V49() FinSequence-like FinSubsequence-like countable FinSequence of the carrier of G
Seg X is V49() X -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= X ) } is set
m | (Seg X) is Relation-like NAT -defined Seg X -defined NAT -defined the carrier of G -valued Function-like V49() FinSubsequence-like countable set
i is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V49() FinSequence-like FinSubsequence-like countable FinSequence of REAL
i | X is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V49() FinSequence-like FinSubsequence-like countable FinSequence of REAL
i | (Seg X) is Relation-like NAT -defined Seg X -defined NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V49() FinSubsequence-like countable set
X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable left_end right_end bounded_below bounded_above real-bounded Element of NAT
len m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
len i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
dom m is V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of K6(NAT)
dom (m | X) is V49() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V49() cardinal V132() V160() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered countable bounded_below bounded_above real-bounded Element of NAT
(i | X) . r is V11() real ext-real Element of REAL
(m | X) /. r is Element of the carrier of G
||.((m | X) /. r).|| is V11() real ext-real non negative Element of REAL
the normF of G . ((m | X) /. r) is V11() real ext-real Element of REAL
i . r is V11() real ext-real Element of REAL
m /. r is Element of the carrier of G
||.(m /. r).|| is V11() real ext-real non negative Element of REAL
the normF of G . (m /. r) is V11() real ext-real Element of REAL
m . r is set
(m | X) . r is