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

{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

{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

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