:: PDIFF_8 semantic presentation

REAL is non empty non finite complex-membered ext-real-membered real-membered V66() non bounded_below non bounded_above V76() set

NAT is non empty V12() V13() V14() non finite V53() V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() left_end bounded_below Element of K10(REAL)

K10(REAL) is non finite set

COMPLEX is non empty non finite complex-membered V66() set

RAT is non empty non finite complex-membered ext-real-membered real-membered rational-membered V66() set

INT is non empty non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V66() set

K11(COMPLEX,COMPLEX) is complex-yielding non finite set

K10(K11(COMPLEX,COMPLEX)) is non finite set

K11(K11(COMPLEX,COMPLEX),COMPLEX) is complex-yielding non finite set

K10(K11(K11(COMPLEX,COMPLEX),COMPLEX)) is non finite set

K11(REAL,REAL) is complex-yielding V37() V38() non finite set

K10(K11(REAL,REAL)) is non finite set

K11(K11(REAL,REAL),REAL) is complex-yielding V37() V38() non finite set

K10(K11(K11(REAL,REAL),REAL)) is non finite set

K11(RAT,RAT) is RAT -valued complex-yielding V37() V38() non finite set

K10(K11(RAT,RAT)) is non finite set

K11(K11(RAT,RAT),RAT) is RAT -valued complex-yielding V37() V38() non finite set

K10(K11(K11(RAT,RAT),RAT)) is non finite set

K11(INT,INT) is RAT -valued INT -valued complex-yielding V37() V38() non finite set

K10(K11(INT,INT)) is non finite set

K11(K11(INT,INT),INT) is RAT -valued INT -valued complex-yielding V37() V38() non finite set

K10(K11(K11(INT,INT),INT)) is non finite set

K11(NAT,NAT) is RAT -valued INT -valued complex-yielding V37() V38() V39() non finite set

K11(K11(NAT,NAT),NAT) is RAT -valued INT -valued complex-yielding V37() V38() V39() non finite set

K10(K11(K11(NAT,NAT),NAT)) is non finite set

NAT is non empty V12() V13() V14() non finite V53() V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() left_end bounded_below set

K10(NAT) is non finite set

K10(NAT) is non finite set

K11(COMPLEX,REAL) is complex-yielding V37() V38() non finite set

K10(K11(COMPLEX,REAL)) is non finite set

K455() is non empty V109() L8()

the carrier of K455() is non empty set

K460() is non empty V109() V131() V132() V133() V135() V161() V162() V163() V164() V165() V166() L8()

K461() is non empty V109() V133() V135() V164() V165() V166() M17(K460())

K462() is non empty V109() V131() V133() V135() V164() V165() V166() V167() M20(K460(),K461())

K464() is non empty V109() V131() V133() V135() L8()

K465() is non empty V109() V131() V133() V135() V167() M17(K464())

K11(NAT,REAL) is complex-yielding V37() V38() non finite set

K10(K11(NAT,REAL)) is non finite set

K496() is non empty set

K11(K496(),K496()) is set

K11(K11(K496(),K496()),K496()) is set

K10(K11(K11(K496(),K496()),K496())) is set

K11(REAL,K496()) is non finite set

K11(K11(REAL,K496()),K496()) is non finite set

K10(K11(K11(REAL,K496()),K496())) is non finite set

K502() is RLSStruct

the carrier of K502() is set

K10( the carrier of K502()) is set

K506() is Element of K10( the carrier of K502())

K11(K506(),K506()) is set

K11(K11(K506(),K506()),REAL) is complex-yielding V37() V38() set

K10(K11(K11(K506(),K506()),REAL)) is set

K509() is Element of K10( the carrier of K502())

K11(K509(),REAL) is complex-yielding V37() V38() set

K10(K11(K509(),REAL)) is set

1 is non empty V12() V13() V14() V18() V19() real ext-real positive non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

K11(1,1) is RAT -valued INT -valued complex-yielding V37() V38() V39() set

K10(K11(1,1)) is set

K11(K11(1,1),1) is RAT -valued INT -valued complex-yielding V37() V38() V39() set

K10(K11(K11(1,1),1)) is set

K11(K11(1,1),REAL) is complex-yielding V37() V38() set

K10(K11(K11(1,1),REAL)) is set

2 is non empty V12() V13() V14() V18() V19() real ext-real positive non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

K11(2,2) is RAT -valued INT -valued complex-yielding V37() V38() V39() set

K11(K11(2,2),REAL) is complex-yielding V37() V38() set

K10(K11(K11(2,2),REAL)) is set

TOP-REAL 2 is non empty V107() V151() V152() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V226() L20()

the carrier of (TOP-REAL 2) is non empty set

REAL 1 is non empty functional FinSequence-membered FinSequenceSet of REAL

1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

K11((REAL 1),(REAL 1)) is set

K10(K11((REAL 1),(REAL 1))) is set

REAL-NS 1 is non empty V86() V107() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V179() V180() V181() V182() V192() L16()

the carrier of (REAL-NS 1) is non empty V2() set

R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)) is non empty V107() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V179() V180() V182() V192() L16()

BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)) is non empty Element of K10( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))))

R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1)) is non empty V107() V151() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

LinearOperators ((REAL-NS 1),(REAL-NS 1)) is non empty functional Element of K10( the carrier of K517( the carrier of (REAL-NS 1),(REAL-NS 1)))

K517( the carrier of (REAL-NS 1),(REAL-NS 1)) is non empty V107() V151() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) is non empty M4( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))

FuncZero ( the carrier of (REAL-NS 1),(REAL-NS 1)) is Relation-like the carrier of (REAL-NS 1) -defined the carrier of (REAL-NS 1) -valued Function-like V32( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) Element of K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))

K401((REAL-NS 1)) is V88( REAL-NS 1) Element of the carrier of (REAL-NS 1)

K237( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1),K401((REAL-NS 1))) is Relation-like the carrier of (REAL-NS 1) -defined the carrier of (REAL-NS 1) -valued Function-like V32( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) Element of K10(K11( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))

K11( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) is set

K10(K11( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) is set

FuncAdd ( the carrier of (REAL-NS 1),(REAL-NS 1)) is Relation-like K11(K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) -defined K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) -valued Function-like V32(K11(K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) Element of K10(K11(K11(K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))))

K11(K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) is set

K11(K11(K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) is set

K10(K11(K11(K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))) is set

FuncExtMult ( the carrier of (REAL-NS 1),(REAL-NS 1)) is Relation-like K11(REAL,K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) -defined K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) -valued Function-like V32(K11(REAL,K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) Element of K10(K11(K11(REAL,K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))))

K11(REAL,K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) is non finite set

K11(K11(REAL,K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) is non finite set

K10(K11(K11(REAL,K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))) is non finite set

RLSStruct(# K165( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)),(FuncZero ( the carrier of (REAL-NS 1),(REAL-NS 1))),(FuncAdd ( the carrier of (REAL-NS 1),(REAL-NS 1))),(FuncExtMult ( the carrier of (REAL-NS 1),(REAL-NS 1))) #) is strict RLSStruct

the carrier of K517( the carrier of (REAL-NS 1),(REAL-NS 1)) is non empty set

K10( the carrier of K517( the carrier of (REAL-NS 1),(REAL-NS 1))) is set

K505(K517( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Relation-like Function-like Element of LinearOperators ((REAL-NS 1),(REAL-NS 1))

K503(K517( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Relation-like K11((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) -defined LinearOperators ((REAL-NS 1),(REAL-NS 1)) -valued Function-like V32(K11((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))), LinearOperators ((REAL-NS 1),(REAL-NS 1))) Element of K10(K11(K11((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))))

K11((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set

K11(K11((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set

K10(K11(K11((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1))))) is set

K504(K517( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Relation-like K11(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) -defined LinearOperators ((REAL-NS 1),(REAL-NS 1)) -valued Function-like V32(K11(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))), LinearOperators ((REAL-NS 1),(REAL-NS 1))) Element of K10(K11(K11(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))))

K11(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is non finite set

K11(K11(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is non finite set

K10(K11(K11(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1))))) is non finite set

RLSStruct(# (LinearOperators ((REAL-NS 1),(REAL-NS 1))),K505(K517( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),K503(K517( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),K504(K517( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) #) is V107() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))) is non empty set

K10( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set

K505((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Element of BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))

K503((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Relation-like K11((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) -defined BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)) -valued Function-like V32(K11((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))), BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) Element of K10(K11(K11((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))))

K11((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set

K11(K11((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set

K10(K11(K11((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))))) is set

K504((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Relation-like K11(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) -defined BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)) -valued Function-like V32(K11(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))), BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) Element of K10(K11(K11(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))))

K11(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is non finite set

K11(K11(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is non finite set

K10(K11(K11(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))))) is non finite set

BoundedLinearOperatorsNorm ((REAL-NS 1),(REAL-NS 1)) is Relation-like BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)) -defined REAL -valued Function-like V32( BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)), REAL ) complex-yielding V37() V38() Element of K10(K11((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),REAL))

K11((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),REAL) is complex-yielding V37() V38() non finite set

K10(K11((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),REAL)) is non finite set

G16((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),K505((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),K503((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),K504((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperatorsNorm ((REAL-NS 1),(REAL-NS 1)))) is V181() L16()

the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) is non empty set

{} is set

the empty V12() V13() V14() V16() V17() V18() V19() real ext-real non positive non negative Function-like functional finite V53() V55( {} ) FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() bounded_below bounded_above real-bounded V76() set is empty V12() V13() V14() V16() V17() V18() V19() real ext-real non positive non negative Function-like functional finite V53() V55( {} ) FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() bounded_below bounded_above real-bounded V76() set

3 is non empty V12() V13() V14() V18() V19() real ext-real positive non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

0 is V12() V13() V14() V18() V19() real ext-real non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

m is V12() V13() V14() V18() V19() real ext-real non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

REAL m is non empty functional FinSequence-membered FinSequenceSet of REAL

m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

TOP-REAL m is non empty V107() V151() V152() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V226() L20()

the carrier of (TOP-REAL m) is non empty set

n is V12() V13() V14() V18() V19() real ext-real non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

Seg m is finite V55(m) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K10(NAT)

{ b

f is Relation-like NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite V55(m) FinSequence-like FinSubsequence-like Element of REAL m

|.f.| is V19() real ext-real non negative Element of REAL

sqr f is Relation-like NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL

Sum (sqr f) is V19() real ext-real Element of REAL

sqrt (Sum (sqr f)) is V19() real ext-real Element of REAL

X is Relation-like NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite V55(m) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL m)

X /. n is V19() real ext-real Element of REAL

abs (X /. n) is V19() real ext-real Element of REAL

0* m is Relation-like NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite V55(m) FinSequence-like FinSubsequence-like Element of REAL m

m |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite V55(m) FinSequence-like FinSubsequence-like Element of m -tuples_on REAL

(X /. n) ^2 is V19() real ext-real Element of REAL

K69((X /. n),(X /. n)) is V19() real ext-real set

(0* m) +* (n,((X /. n) ^2)) is Relation-like NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL

Sum ((0* m) +* (n,((X /. n) ^2))) is V19() real ext-real Element of REAL

len (0* m) is V12() V13() V14() V18() V19() real ext-real non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

len ((0* m) +* (n,((X /. n) ^2))) is V12() V13() V14() V18() V19() real ext-real non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

i is Relation-like NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite V55(m) FinSequence-like FinSubsequence-like Element of m -tuples_on REAL

len i is V12() V13() V14() V18() V19() real ext-real non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

sqr f is Relation-like NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite V55(m) FinSequence-like FinSubsequence-like Element of m -tuples_on REAL

Sum (sqr f) is V19() real ext-real Element of REAL

len f is V12() V13() V14() V18() V19() real ext-real non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

j is Relation-like NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite V55(m) FinSequence-like FinSubsequence-like Element of m -tuples_on REAL

r is V12() V13() V14() V18() V19() real ext-real non negative finite V53() set

i . r is V19() real ext-real Element of REAL

j . r is V19() real ext-real Element of REAL

dom f is V55(m) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of K10(NAT)

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

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

dom (0* m) is V55(m) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of K10(NAT)

Seg (len (0* m)) is finite V55( len (0* m)) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K10(NAT)

{ b

dom i is V55(m) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of K10(NAT)

i /. n is V19() real ext-real Element of REAL

f /. n is V19() real ext-real Element of REAL

(f /. n) ^2 is V19() real ext-real Element of REAL

K69((f /. n),(f /. n)) is V19() real ext-real set

dom (0* m) is V55(m) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of K10(NAT)

Seg (len (0* m)) is finite V55( len (0* m)) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K10(NAT)

{ b

dom f is V55(m) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of K10(NAT)

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

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

(f /. r) ^2 is V19() real ext-real Element of REAL

K69((f /. r),(f /. r)) is V19() real ext-real set

dom i is V55(m) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of K10(NAT)

i /. r is V19() real ext-real Element of REAL

(0* m) /. r is V19() real ext-real Element of REAL

m |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like complex-yielding V37() V38() V39() finite V55(m) FinSequence-like FinSubsequence-like Element of m -tuples_on NAT

m -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT

(m |-> 0) . r is empty V12() V13() V14() V16() V17() V18() V19() real ext-real non positive non negative Function-like functional finite V53() V55( {} ) FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() bounded_below bounded_above real-bounded V76() Element of REAL

Sum i is V19() real ext-real Element of REAL

Sum j is V19() real ext-real Element of REAL

sqrt (Sum (sqr f)) is V19() real ext-real Element of REAL

(sqrt (Sum (sqr f))) ^2 is V19() real ext-real Element of REAL

K69((sqrt (Sum (sqr f))),(sqrt (Sum (sqr f)))) is V19() real ext-real set

sqrt ((X /. n) ^2) is V19() real ext-real Element of REAL

sqrt ((sqrt (Sum (sqr f))) ^2) is V19() real ext-real Element of REAL

abs (abs (X /. n)) is V19() real ext-real Element of REAL

abs (sqrt (Sum (sqr f))) is V19() real ext-real Element of REAL

m is V19() real ext-real Element of REAL

<*m*> is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant complex-yielding V37() V38() V40() V41() V42() V43() finite V55(1) FinSequence-like FinSubsequence-like FinSequence of REAL

[1,m] is set

{[1,m]} is non empty V2() Function-like V55(1) set

abs m is V19() real ext-real Element of REAL

n is Element of the carrier of (REAL-NS 1)

||.n.|| is V19() real ext-real Element of REAL

the U9 of (REAL-NS 1) is Relation-like the carrier of (REAL-NS 1) -defined REAL -valued Function-like V32( the carrier of (REAL-NS 1), REAL ) complex-yielding V37() V38() Element of K10(K11( the carrier of (REAL-NS 1),REAL))

K11( the carrier of (REAL-NS 1),REAL) is complex-yielding V37() V38() non finite set

K10(K11( the carrier of (REAL-NS 1),REAL)) is non finite set

the U9 of (REAL-NS 1) . n is V19() real ext-real Element of REAL

f is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant complex-yielding V37() V38() V40() V41() V42() V43() finite V55(1) FinSequence-like FinSubsequence-like Element of REAL 1

sqr f is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant complex-yielding V37() V38() V40() V41() V42() V43() finite V55(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on REAL

Sum (sqr f) is V19() real ext-real Element of REAL

sqrt (Sum (sqr f)) is V19() real ext-real Element of REAL

m ^2 is V19() real ext-real Element of REAL

K69(m,m) is V19() real ext-real set

<*(m ^2)*> is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant complex-yielding V37() V38() V40() V41() V42() V43() finite V55(1) FinSequence-like FinSubsequence-like FinSequence of REAL

[1,(m ^2)] is set

{[1,(m ^2)]} is non empty V2() Function-like V55(1) set

Sum <*(m ^2)*> is V19() real ext-real Element of REAL

sqrt (Sum <*(m ^2)*>) is V19() real ext-real Element of REAL

sqrt (m ^2) is V19() real ext-real Element of REAL

|.f.| is V19() real ext-real non negative Element of REAL

sqr f is Relation-like NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL

Sum (sqr f) is V19() real ext-real Element of REAL

sqrt (Sum (sqr f)) is V19() real ext-real Element of REAL

m is non empty V12() V13() V14() V18() V19() real ext-real positive non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

REAL-NS m is non empty V86() V107() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V179() V180() V181() V182() V192() L16()

the carrier of (REAL-NS m) is non empty V2() set

n is Element of the carrier of (REAL-NS m)

||.n.|| is V19() real ext-real Element of REAL

the U9 of (REAL-NS m) is Relation-like the carrier of (REAL-NS m) -defined REAL -valued Function-like V32( the carrier of (REAL-NS m), REAL ) complex-yielding V37() V38() Element of K10(K11( the carrier of (REAL-NS m),REAL))

K11( the carrier of (REAL-NS m),REAL) is complex-yielding V37() V38() non finite set

K10(K11( the carrier of (REAL-NS m),REAL)) is non finite set

the U9 of (REAL-NS m) . n is V19() real ext-real Element of REAL

f is V12() V13() V14() V18() V19() real ext-real non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

Proj (f,m) is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS 1) -valued Function-like V32( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)) Element of K10(K11( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)))

K11( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)) is set

K10(K11( the carrier of (REAL-NS m), the carrier of (REAL-NS 1))) is set

(Proj (f,m)) . n is Element of the carrier of (REAL-NS 1)

||.((Proj (f,m)) . n).|| is V19() real ext-real Element of REAL

the U9 of (REAL-NS 1) is Relation-like the carrier of (REAL-NS 1) -defined REAL -valued Function-like V32( the carrier of (REAL-NS 1), REAL ) complex-yielding V37() V38() Element of K10(K11( the carrier of (REAL-NS 1),REAL))

K11( the carrier of (REAL-NS 1),REAL) is complex-yielding V37() V38() non finite set

K10(K11( the carrier of (REAL-NS 1),REAL)) is non finite set

the U9 of (REAL-NS 1) . ((Proj (f,m)) . n) is V19() real ext-real Element of REAL

REAL m is non empty functional FinSequence-membered FinSequenceSet of REAL

m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

X is Relation-like NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite V55(m) FinSequence-like FinSubsequence-like Element of REAL m

|.X.| is V19() real ext-real non negative Element of REAL

sqr X is Relation-like NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL

Sum (sqr X) is V19() real ext-real Element of REAL

sqrt (Sum (sqr X)) is V19() real ext-real Element of REAL

proj (f,m) is Relation-like REAL m -defined REAL -valued Function-like V32( REAL m, REAL ) complex-yielding V37() V38() Element of K10(K11((REAL m),REAL))

K11((REAL m),REAL) is complex-yielding V37() V38() non finite set

K10(K11((REAL m),REAL)) is non finite set

(proj (f,m)) . n is V19() real ext-real Element of REAL

<*((proj (f,m)) . n)*> is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant complex-yielding V37() V38() V40() V41() V42() V43() finite V55(1) FinSequence-like FinSubsequence-like FinSequence of REAL

[1,((proj (f,m)) . n)] is set

{[1,((proj (f,m)) . n)]} is non empty V2() Function-like V55(1) set

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

<*(X . f)*> is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant complex-yielding V37() V38() V40() V41() V42() V43() finite V55(1) FinSequence-like FinSubsequence-like FinSequence of REAL

[1,(X . f)] is set

{[1,(X . f)]} is non empty V2() Function-like V55(1) set

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

TOP-REAL m is non empty V107() V151() V152() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V226() L20()

the carrier of (TOP-REAL m) is non empty set

Seg m is non empty finite V55(m) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of K10(NAT)

{ b

i is Relation-like NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite V55(m) FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL m)

i /. f is V19() real ext-real Element of REAL

abs (i /. f) is V19() real ext-real Element of REAL

dom X is V55(m) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of K10(NAT)

m is non empty V12() V13() V14() V18() V19() real ext-real positive non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

REAL-NS m is non empty V86() V107() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V179() V180() V181() V182() V192() L16()

the carrier of (REAL-NS m) is non empty V2() set

n is Element of the carrier of (REAL-NS m)

f is V12() V13() V14() V18() V19() real ext-real non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

Proj (f,m) is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS 1) -valued Function-like V32( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)) Element of K10(K11( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)))

K11( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)) is set

K10(K11( the carrier of (REAL-NS m), the carrier of (REAL-NS 1))) is set

(Proj (f,m)) . n is Element of the carrier of (REAL-NS 1)

||.((Proj (f,m)) . n).|| is V19() real ext-real Element of REAL

the U9 of (REAL-NS 1) is Relation-like the carrier of (REAL-NS 1) -defined REAL -valued Function-like V32( the carrier of (REAL-NS 1), REAL ) complex-yielding V37() V38() Element of K10(K11( the carrier of (REAL-NS 1),REAL))

K11( the carrier of (REAL-NS 1),REAL) is complex-yielding V37() V38() non finite set

K10(K11( the carrier of (REAL-NS 1),REAL)) is non finite set

the U9 of (REAL-NS 1) . ((Proj (f,m)) . n) is V19() real ext-real Element of REAL

proj (f,m) is Relation-like REAL m -defined REAL -valued Function-like V32( REAL m, REAL ) complex-yielding V37() V38() Element of K10(K11((REAL m),REAL))

REAL m is non empty functional FinSequence-membered FinSequenceSet of REAL

m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

K11((REAL m),REAL) is complex-yielding V37() V38() non finite set

K10(K11((REAL m),REAL)) is non finite set

(proj (f,m)) . n is V19() real ext-real Element of REAL

|.((proj (f,m)) . n).| is V19() real ext-real Element of REAL

<*((proj (f,m)) . n)*> is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant complex-yielding V37() V38() V40() V41() V42() V43() finite V55(1) FinSequence-like FinSubsequence-like FinSequence of REAL

[1,((proj (f,m)) . n)] is set

{[1,((proj (f,m)) . n)]} is non empty V2() Function-like V55(1) set

X is Relation-like NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite V55(m) FinSequence-like FinSubsequence-like Element of REAL m

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

<*(X . f)*> is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant complex-yielding V37() V38() V40() V41() V42() V43() finite V55(1) FinSequence-like FinSubsequence-like FinSequence of REAL

[1,(X . f)] is set

{[1,(X . f)]} is non empty V2() Function-like V55(1) set

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

m is non empty V12() V13() V14() V18() V19() real ext-real positive non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

REAL m is non empty functional FinSequence-membered FinSequenceSet of REAL

m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL

n is Relation-like NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite V55(m) FinSequence-like FinSubsequence-like Element of REAL m

|.n.| is V19() real ext-real non negative Element of REAL

sqr n is Relation-like NAT -defined REAL -valued Function-like complex-yielding V37() V38() finite FinSequence-like FinSubsequence-like FinSequence of REAL

Sum (sqr n) is V19() real ext-real Element of REAL

sqrt (Sum (sqr n)) is V19() real ext-real Element of REAL

f is V12() V13() V14() V18() V19() real ext-real non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

proj (f,m) is Relation-like REAL m -defined REAL -valued Function-like V32( REAL m, REAL ) complex-yielding V37() V38() Element of K10(K11((REAL m),REAL))

K11((REAL m),REAL) is complex-yielding V37() V38() non finite set

K10(K11((REAL m),REAL)) is non finite set

(proj (f,m)) . n is V19() real ext-real Element of REAL

|.((proj (f,m)) . n).| is V19() real ext-real Element of REAL

REAL-NS m is non empty V86() V107() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V179() V180() V181() V182() V192() L16()

the carrier of (REAL-NS m) is non empty V2() set

Proj (f,m) is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS 1) -valued Function-like V32( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)) Element of K10(K11( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)))

K11( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)) is set

K10(K11( the carrier of (REAL-NS m), the carrier of (REAL-NS 1))) is set

X is Element of the carrier of (REAL-NS m)

(Proj (f,m)) . X is Element of the carrier of (REAL-NS 1)

||.((Proj (f,m)) . X).|| is V19() real ext-real Element of REAL

the U9 of (REAL-NS 1) is Relation-like the carrier of (REAL-NS 1) -defined REAL -valued Function-like V32( the carrier of (REAL-NS 1), REAL ) complex-yielding V37() V38() Element of K10(K11( the carrier of (REAL-NS 1),REAL))

K11( the carrier of (REAL-NS 1),REAL) is complex-yielding V37() V38() non finite set

K10(K11( the carrier of (REAL-NS 1),REAL)) is non finite set

the U9 of (REAL-NS 1) . ((Proj (f,m)) . X) is V19() real ext-real Element of REAL

(proj (f,m)) . X is V19() real ext-real Element of REAL

|.((proj (f,m)) . X).| is V19() real ext-real Element of REAL

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

the U9 of (REAL-NS m) is Relation-like the carrier of (REAL-NS m) -defined REAL -valued Function-like V32( the carrier of (REAL-NS m), REAL ) complex-yielding V37() V38() Element of K10(K11( the carrier of (REAL-NS m),REAL))

K11( the carrier of (REAL-NS m),REAL) is complex-yielding V37() V38() non finite set

K10(K11( the carrier of (REAL-NS m),REAL)) is non finite set

the U9 of (REAL-NS m) . X is V19() real ext-real Element of REAL

m is non empty V12() V13() V14() V18() V19() real ext-real positive non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

REAL-NS m is non empty V86() V107() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V179() V180() V181() V182() V192() L16()

n is non empty V12() V13() V14() V18() V19() real ext-real positive non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

REAL-NS n is non empty V86() V107() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V179() V180() V181() V182() V192() L16()

R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) is non empty V107() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V179() V180() V182() V192() L16()

BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) is non empty Element of K10( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))))

R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n)) is non empty V107() V151() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

LinearOperators ((REAL-NS m),(REAL-NS n)) is non empty functional Element of K10( the carrier of K517( the carrier of (REAL-NS m),(REAL-NS n)))

the carrier of (REAL-NS m) is non empty V2() set

K517( the carrier of (REAL-NS m),(REAL-NS n)) is non empty V107() V151() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of (REAL-NS n) is non empty V2() set

K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) is non empty M4( the carrier of (REAL-NS m), the carrier of (REAL-NS n))

FuncZero ( the carrier of (REAL-NS m),(REAL-NS n)) is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS n) -valued Function-like V32( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) Element of K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))

K401((REAL-NS n)) is V88( REAL-NS n) Element of the carrier of (REAL-NS n)

K237( the carrier of (REAL-NS n), the carrier of (REAL-NS m),K401((REAL-NS n))) is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS n) -valued Function-like V32( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) Element of K10(K11( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))

K11( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) is set

K10(K11( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is set

FuncAdd ( the carrier of (REAL-NS m),(REAL-NS n)) is Relation-like K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) -defined K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) -valued Function-like V32(K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) Element of K10(K11(K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))))

K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is set

K11(K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is set

K10(K11(K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))) is set

FuncExtMult ( the carrier of (REAL-NS m),(REAL-NS n)) is Relation-like K11(REAL,K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) -defined K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) -valued Function-like V32(K11(REAL,K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) Element of K10(K11(K11(REAL,K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))))

K11(REAL,K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is non finite set

K11(K11(REAL,K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is non finite set

K10(K11(K11(REAL,K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))) is non finite set

RLSStruct(# K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),(FuncZero ( the carrier of (REAL-NS m),(REAL-NS n))),(FuncAdd ( the carrier of (REAL-NS m),(REAL-NS n))),(FuncExtMult ( the carrier of (REAL-NS m),(REAL-NS n))) #) is strict RLSStruct

the carrier of K517( the carrier of (REAL-NS m),(REAL-NS n)) is non empty set

K10( the carrier of K517( the carrier of (REAL-NS m),(REAL-NS n))) is set

K505(K517( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like Function-like Element of LinearOperators ((REAL-NS m),(REAL-NS n))

K503(K517( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K11((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))) -defined LinearOperators ((REAL-NS m),(REAL-NS n)) -valued Function-like V32(K11((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))), LinearOperators ((REAL-NS m),(REAL-NS n))) Element of K10(K11(K11((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))))

K11((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is set

K11(K11((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is set

K10(K11(K11((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n))))) is set

K504(K517( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K11(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))) -defined LinearOperators ((REAL-NS m),(REAL-NS n)) -valued Function-like V32(K11(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))), LinearOperators ((REAL-NS m),(REAL-NS n))) Element of K10(K11(K11(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))))

K11(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))) is non finite set

K11(K11(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is non finite set

K10(K11(K11(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n))))) is non finite set

RLSStruct(# (LinearOperators ((REAL-NS m),(REAL-NS n))),K505(K517( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))),K503(K517( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))),K504(K517( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) #) is V107() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))) is non empty set

K10( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n)))) is set

K505((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is Element of BoundedLinearOperators ((REAL-NS m),(REAL-NS n))

K503((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) -defined BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) -valued Function-like V32(K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))), BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) Element of K10(K11(K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))))

K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is set

K11(K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is set

K10(K11(K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n))))) is set

K504((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K11(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) -defined BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) -valued Function-like V32(K11(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))), BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) Element of K10(K11(K11(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))))

K11(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is non finite set

K11(K11(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is non finite set

K10(K11(K11(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n))))) is non finite set

BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS n)) is Relation-like BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) -defined REAL -valued Function-like V32( BoundedLinearOperators ((REAL-NS m),(REAL-NS n)), REAL ) complex-yielding V37() V38() Element of K10(K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),REAL))

K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),REAL) is complex-yielding V37() V38() non finite set

K10(K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),REAL)) is non finite set

G16((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),K505((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),K503((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),K504((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS n)))) is V181() L16()

the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) is non empty set

K11( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)) is set

K10(K11( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))) is set

BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1)) is Relation-like BoundedLinearOperators ((REAL-NS n),(REAL-NS 1)) -defined REAL -valued Function-like V32( BoundedLinearOperators ((REAL-NS n),(REAL-NS 1)), REAL ) complex-yielding V37() V38() Element of K10(K11((BoundedLinearOperators ((REAL-NS n),(REAL-NS 1))),REAL))

BoundedLinearOperators ((REAL-NS n),(REAL-NS 1)) is non empty Element of K10( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS n),(REAL-NS 1))))

R_VectorSpace_of_LinearOperators ((REAL-NS n),(REAL-NS 1)) is non empty V107() V151() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

LinearOperators ((REAL-NS n),(REAL-NS 1)) is non empty functional Element of K10( the carrier of K517( the carrier of (REAL-NS n),(REAL-NS 1)))

K517( the carrier of (REAL-NS n),(REAL-NS 1)) is non empty V107() V151() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)) is non empty M4( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))

FuncZero ( the carrier of (REAL-NS n),(REAL-NS 1)) is Relation-like the carrier of (REAL-NS n) -defined the carrier of (REAL-NS 1) -valued Function-like V32( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)) Element of K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))

K237( the carrier of (REAL-NS 1), the carrier of (REAL-NS n),K401((REAL-NS 1))) is Relation-like the carrier of (REAL-NS n) -defined the carrier of (REAL-NS 1) -valued Function-like V32( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)) Element of K10(K11( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)))

FuncAdd ( the carrier of (REAL-NS n),(REAL-NS 1)) is Relation-like K11(K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))) -defined K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)) -valued Function-like V32(K11(K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))) Element of K10(K11(K11(K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))))

K11(K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))) is set

K11(K11(K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))) is set

K10(K11(K11(K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)))) is set

FuncExtMult ( the carrier of (REAL-NS n),(REAL-NS 1)) is Relation-like K11(REAL,K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))) -defined K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)) -valued Function-like V32(K11(REAL,K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))) Element of K10(K11(K11(REAL,K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))))

K11(REAL,K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))) is non finite set

K11(K11(REAL,K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))) is non finite set

K10(K11(K11(REAL,K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)))) is non finite set

RLSStruct(# K165( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)),(FuncZero ( the carrier of (REAL-NS n),(REAL-NS 1))),(FuncAdd ( the carrier of (REAL-NS n),(REAL-NS 1))),(FuncExtMult ( the carrier of (REAL-NS n),(REAL-NS 1))) #) is strict RLSStruct

the carrier of K517( the carrier of (REAL-NS n),(REAL-NS 1)) is non empty set

K10( the carrier of K517( the carrier of (REAL-NS n),(REAL-NS 1))) is set

K505(K517( the carrier of (REAL-NS n),(REAL-NS 1)),(LinearOperators ((REAL-NS n),(REAL-NS 1)))) is Relation-like Function-like Element of LinearOperators ((REAL-NS n),(REAL-NS 1))

K503(K517( the carrier of (REAL-NS n),(REAL-NS 1)),(LinearOperators ((REAL-NS n),(REAL-NS 1)))) is Relation-like K11((LinearOperators ((REAL-NS n),(REAL-NS 1))),(LinearOperators ((REAL-NS n),(REAL-NS 1)))) -defined LinearOperators ((REAL-NS n),(REAL-NS 1)) -valued Function-like V32(K11((LinearOperators ((REAL-NS n),(REAL-NS 1))),(LinearOperators ((REAL-NS n),(REAL-NS 1)))), LinearOperators ((REAL-NS n),(REAL-NS 1))) Element of K10(K11(K11((LinearOperators ((REAL-NS n),(REAL-NS 1))),(LinearOperators ((REAL-NS n),(REAL-NS 1)))),(LinearOperators ((REAL-NS n),(REAL-NS 1)))))

K11((LinearOperators ((REAL-NS n),(REAL-NS 1))),(LinearOperators ((REAL-NS n),(REAL-NS 1)))) is set

K11(K11((LinearOperators ((REAL-NS n),(REAL-NS 1))),(LinearOperators ((REAL-NS n),(REAL-NS 1)))),(LinearOperators ((REAL-NS n),(REAL-NS 1)))) is set

K10(K11(K11((LinearOperators ((REAL-NS n),(REAL-NS 1))),(LinearOperators ((REAL-NS n),(REAL-NS 1)))),(LinearOperators ((REAL-NS n),(REAL-NS 1))))) is set

K504(K517( the carrier of (REAL-NS n),(REAL-NS 1)),(LinearOperators ((REAL-NS n),(REAL-NS 1)))) is Relation-like K11(REAL,(LinearOperators ((REAL-NS n),(REAL-NS 1)))) -defined LinearOperators ((REAL-NS n),(REAL-NS 1)) -valued Function-like V32(K11(REAL,(LinearOperators ((REAL-NS n),(REAL-NS 1)))), LinearOperators ((REAL-NS n),(REAL-NS 1))) Element of K10(K11(K11(REAL,(LinearOperators ((REAL-NS n),(REAL-NS 1)))),(LinearOperators ((REAL-NS n),(REAL-NS 1)))))

K11(REAL,(LinearOperators ((REAL-NS n),(REAL-NS 1)))) is non finite set

K11(K11(REAL,(LinearOperators ((REAL-NS n),(REAL-NS 1)))),(LinearOperators ((REAL-NS n),(REAL-NS 1)))) is non finite set

K10(K11(K11(REAL,(LinearOperators ((REAL-NS n),(REAL-NS 1)))),(LinearOperators ((REAL-NS n),(REAL-NS 1))))) is non finite set

RLSStruct(# (LinearOperators ((REAL-NS n),(REAL-NS 1))),K505(K517( the carrier of (REAL-NS n),(REAL-NS 1)),(LinearOperators ((REAL-NS n),(REAL-NS 1)))),K503(K517( the carrier of (REAL-NS n),(REAL-NS 1)),(LinearOperators ((REAL-NS n),(REAL-NS 1)))),K504(K517( the carrier of (REAL-NS n),(REAL-NS 1)),(LinearOperators ((REAL-NS n),(REAL-NS 1)))) #) is V107() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS n),(REAL-NS 1))) is non empty set

K10( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS n),(REAL-NS 1)))) is set

K11((BoundedLinearOperators ((REAL-NS n),(REAL-NS 1))),REAL) is complex-yielding V37() V38() non finite set

K10(K11((BoundedLinearOperators ((REAL-NS n),(REAL-NS 1))),REAL)) is non finite set

X is V12() V13() V14() V18() V19() real ext-real non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT

Proj (X,n) is Relation-like the carrier of (REAL-NS n) -defined the carrier of (REAL-NS 1) -valued Function-like V32( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)) Element of K10(K11( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)))

(BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS 1))) . (Proj (X,n)) is V19() real ext-real Element of REAL

i is Element of the carrier of (REAL-NS n)

j is V19() real ext-real Element of REAL

j * i is Element of the carrier of (REAL-NS n)

(Proj (X,n)) . (j * i) is Element of the carrier of (REAL-NS 1)

(Proj (X,n)) . i is Element of the carrier of (REAL-NS 1)

j * ((Proj (X,n)) . i) is Element of the carrier of (REAL-NS 1)

i is Element of the carrier of (REAL-NS n)

j is Element of the carrier of (REAL-NS n)

i + j is Element of the carrier of (REAL-NS n)

(Proj (X,n)) . (i + j) is Element of the carrier of (REAL-NS 1)

(Proj (X,n)) . i is Element of the carrier of (REAL-NS 1)

(Proj (X,n)) . j is Element of the carrier of (REAL-NS 1)

((Proj (X,n)) . i) + ((Proj (X,n)) . j) is Element of the carrier of (REAL-NS 1)

modetrans ((Proj (X,n)),(REAL-NS n),(REAL-NS 1)) is Relation-like the carrier of (REAL-NS n) -defined the carrier of (REAL-NS 1) -valued Function-like V32( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)) V149( REAL-NS n, REAL-NS 1) homogeneous Lipschitzian Element of K10(K11( the carrier of (REAL-NS n), the carrier of (REAL-NS 1)))

PreNorms (modetrans ((Proj (X,n)),(REAL-NS n),(REAL-NS 1))) is non empty complex-membered ext-real-membered real-membered Element of K10(REAL)

{ ||.((modetrans ((Proj (X,n)),(REAL-NS n),(REAL-NS 1))) . b

upper_bound (PreNorms (modetrans ((Proj (X,n)),(REAL-NS n),(REAL-NS 1)))) is V19() real ext-real Element of REAL

j is V19() real ext-real set

r is Element of the carrier of (REAL-NS n)

(modetrans ((Proj (X,n)),(REAL-NS n),(REAL-NS 1))) . r is Element of the carrier of (REAL-NS 1)

||.((modetrans ((Proj (X,n)),(REAL-NS n),(REAL-NS 1))) . r).|| is V19() real ext-real Element of REAL

the U9 of (REAL-NS 1) is Relation-like the carrier of (REAL-NS 1) -defined REAL -valued Function-like V32( the carrier of (REAL-NS 1), REAL ) complex-yielding V37() V38() Element of K10(K11( the carrier of (REAL-NS 1),REAL))

K11( the carrier of (REAL-NS 1),REAL) is complex-yielding V37() V38() non finite set

K10(K11( the carrier of (REAL-NS 1),REAL)) is non finite set

the U9 of (REAL-NS 1) . ((modetrans ((Proj (X,n)),(REAL-NS n),(REAL-NS 1))) . r) is V19() real ext-real Element of REAL

||.r.|| is V19() real ext-real Element of REAL

the U9 of (REAL-NS n) is Relation-like the carrier of (REAL-NS n) -defined REAL -valued Function-like V32( the carrier of (REAL-NS n), REAL ) complex-yielding V37() V38() Element of K10(K11( the carrier of (REAL-NS n),REAL))

K11( the carrier of (REAL-NS n),REAL) is complex-yielding V37() V38() non finite set

K10(K11( the carrier of (REAL-NS n),REAL)) is non finite set

the U9 of (REAL-NS n) . r is V19() real ext-real Element of REAL

(Proj (X,n)) . r is Element of the carrier of (REAL-NS 1)

||.((Proj (X,n)) . r).|| is V19() real ext-real Element of REAL

the U9 of (REAL-NS 1) . ((Proj (X,n)) . r) is V19() real ext-real Element of REAL

j is ext-real set

(upper_bound (PreNorms (modetrans ((Proj (X,n)),(REAL-NS n),(REAL-NS 1))))) - 1 is V19() real ext-real Element of REAL

(upper_bound (PreNorms (modetrans ((Proj (X,n)),(REAL-NS n),(REAL-NS 1))))) - ((upper_bound (PreNorms (modetrans ((Proj (X,n)),(REAL-NS n),(REAL-NS 1))))) - 1) is V19() real ext-real Element of REAL

r is V19() real ext-real set

m is non empty V12() V13() V14() V18() V19() real ext-real positive non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

REAL-NS m is non empty V86() V107() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V179() V180() V181() V182() V192() L16()

n is non empty V12() V13() V14() V18() V19() real ext-real positive non negative V24() V35() finite V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT

REAL-NS n is non empty V86() V107() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V179() V180() V181() V182() V192() L16()

R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) is non empty V107() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V179() V180() V182() V192() L16()

BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) is non empty Element of K10( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))))

R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n)) is non empty V107() V151() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

LinearOperators ((REAL-NS m),(REAL-NS n)) is non empty functional Element of K10( the carrier of K517( the carrier of (REAL-NS m),(REAL-NS n)))

the carrier of (REAL-NS m) is non empty V2() set

K517( the carrier of (REAL-NS m),(REAL-NS n)) is non empty V107() V151() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of (REAL-NS n) is non empty V2() set

K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) is non empty M4( the carrier of (REAL-NS m), the carrier of (REAL-NS n))

FuncZero ( the carrier of (REAL-NS m),(REAL-NS n)) is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS n) -valued Function-like V32( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) Element of K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))

K401((REAL-NS n)) is V88( REAL-NS n) Element of the carrier of (REAL-NS n)

K237( the carrier of (REAL-NS n), the carrier of (REAL-NS m),K401((REAL-NS n))) is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS n) -valued Function-like V32( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) Element of K10(K11( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))

K11( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) is set

K10(K11( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is set

FuncAdd ( the carrier of (REAL-NS m),(REAL-NS n)) is Relation-like K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) -defined K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) -valued Function-like V32(K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) Element of K10(K11(K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))))

K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is set

K11(K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is set

K10(K11(K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))) is set

FuncExtMult ( the carrier of (REAL-NS m),(REAL-NS n)) is Relation-like K11(REAL,K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) -defined K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) -valued Function-like V32(K11(REAL,K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) Element of K10(K11(K11(REAL,K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))))

K11(REAL,K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is non finite set

K11(K11(REAL,K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is non finite set

K10(K11(K11(REAL,K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))) is non finite set

RLSStruct(# K165( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),(FuncZero ( the carrier of (REAL-NS m),(REAL-NS n))),(FuncAdd ( the carrier of (REAL-NS m),(REAL-NS n))),(FuncExtMult ( the carrier of (REAL-NS m),(REAL-NS n))) #) is strict RLSStruct

the carrier of K517( the carrier of (REAL-NS m),(REAL-NS n)) is non empty set

K10( the carrier of K517( the carrier of (REAL-NS m),(REAL-NS n))) is set

K505(K517( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like Function-like Element of LinearOperators ((REAL-NS m),(REAL-NS n))

K503(K517( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K11((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))) -defined LinearOperators ((REAL-NS m),(REAL-NS n)) -valued Function-like V32(K11((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))), LinearOperators ((REAL-NS m),(REAL-NS n))) Element of K10(K11(K11((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))))

K11((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is set

K11(K11((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is set

K10(K11(K11((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n))))) is set

K504(K517( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K11(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))) -defined LinearOperators ((REAL-NS m),(REAL-NS n)) -valued Function-like V32(K11(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))), LinearOperators ((REAL-NS m),(REAL-NS n))) Element of K10(K11(K11(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))))

K11(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))) is non finite set

K11(K11(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is non finite set

K10(K11(K11(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n))))) is non finite set

RLSStruct(# (LinearOperators ((REAL-NS m),(REAL-NS n))),K505(K517( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))),K503(K517( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))),K504(K517( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) #) is V107() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))) is non empty set

K10( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n)))) is set

K505((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is Element of BoundedLinearOperators ((REAL-NS m),(REAL-NS n))

K503((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) -defined BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) -valued Function-like V32(K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))), BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) Element of K10(K11(K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))))

K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is set

K11(K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is set

K10(K11(K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n))))) is set

K504((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K11(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) -defined BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) -valued Function-like V32(K11(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))), BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) Element of K10(K11(K11(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))))

K11(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is non finite set

K11(K11(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is non finite set

K10(K11(K11(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n))))) is non finite set

BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS n)) is Relation-like BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) -defined REAL -valued Function-like V32( BoundedLinearOperators ((REAL-NS m),(REAL-NS n)), REAL ) complex-yielding V37() V38() Element of K10(K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),REAL))

K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),REAL) is complex-yielding V37() V38() non finite set

K10(K11((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),REAL)) is non finite set

G16((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),K505((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),K503((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),K504((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS n)))) is V181() L16()

the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) is non empty set

R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1)) is non empty V107() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V179() V180() V182() V192() L16()

BoundedLinearOperators ((REAL-NS m),(REAL-NS 1)) is non empty Element of K10( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS 1))))

R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS 1)) is non empty V107() V151() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

LinearOperators ((REAL-NS m),(REAL-NS 1)) is non empty functional Element of K10( the carrier of K517( the carrier of (REAL-NS m),(REAL-NS 1)))

K517( the carrier of (REAL-NS m),(REAL-NS 1)) is non empty V107() V151() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)) is non empty M4( the carrier of (REAL-NS m), the carrier of (REAL-NS 1))

FuncZero ( the carrier of (REAL-NS m),(REAL-NS 1)) is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS 1) -valued Function-like V32( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)) Element of K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1))

K237( the carrier of (REAL-NS 1), the carrier of (REAL-NS m),K401((REAL-NS 1))) is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS 1) -valued Function-like V32( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)) Element of K10(K11( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)))

K11( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)) is set

K10(K11( the carrier of (REAL-NS m), the carrier of (REAL-NS 1))) is set

FuncAdd ( the carrier of (REAL-NS m),(REAL-NS 1)) is Relation-like K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1))) -defined K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)) -valued Function-like V32(K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1))) Element of K10(K11(K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1))))

K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1))) is set

K11(K11(K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1)),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1))),K165( the carrier of (REAL-NS m), the carrier of (REAL-NS 1))) is set

K10(K11(K11(K165( the carrier of (REAL-NS m), the carrier of