REAL is non empty V33() V156() V157() V158() V162() set
NAT is V6() V33() V38() V39() V156() V157() V158() V159() V160() V161() V162() Element of K6(REAL)
K6(REAL) is V33() set
REAL * is functional FinSequence-membered FinSequenceSet of REAL
K7(NAT,(REAL *)) is set
K6(K7(NAT,(REAL *))) is set
COMPLEX is non empty V33() V156() V162() set
NAT is V6() V33() V38() V39() V156() V157() V158() V159() V160() V161() V162() set
K6(NAT) is V33() set
K6(NAT) is V33() set
K7(NAT,REAL) is V33() complex-yielding V146() V147() set
K6(K7(NAT,REAL)) is V33() set
K190() is non empty set
K7(K190(),K190()) is set
K7(K7(K190(),K190()),K190()) is set
K6(K7(K7(K190(),K190()),K190())) is set
K7(REAL,K190()) is V33() set
K7(K7(REAL,K190()),K190()) is V33() set
K6(K7(K7(REAL,K190()),K190())) is V33() set
K196() is RLSStruct
the carrier of K196() is set
K6( the carrier of K196()) is set
K200() is Element of K6( the carrier of K196())
K7(K200(),K200()) is set
K7(K7(K200(),K200()),REAL) is complex-yielding V146() V147() set
K6(K7(K7(K200(),K200()),REAL)) is set
K203() is Element of K6( the carrier of K196())
K7(K203(),REAL) is complex-yielding V146() V147() set
K6(K7(K203(),REAL)) is set
RAT is non empty V33() V156() V157() V158() V159() V162() set
INT is non empty V33() V156() V157() V158() V159() V160() V162() set
1 is non empty V6() V10() V11() V12() ext-real positive non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
K7(1,1) is RAT -valued INT -valued complex-yielding V146() V147() V148() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is RAT -valued INT -valued complex-yielding V146() V147() V148() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is complex-yielding V146() V147() set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is V33() complex-yielding V146() V147() set
K7(K7(REAL,REAL),REAL) is V33() complex-yielding V146() V147() set
K6(K7(K7(REAL,REAL),REAL)) is V33() set
2 is non empty V6() V10() V11() V12() ext-real positive non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
K7(2,2) is RAT -valued INT -valued complex-yielding V146() V147() V148() set
K7(K7(2,2),REAL) is complex-yielding V146() V147() set
K6(K7(K7(2,2),REAL)) is set
K6(K7(REAL,REAL)) is V33() set
TOP-REAL 2 is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V198() V205() L20()
the carrier of (TOP-REAL 2) is non empty set
REAL 1 is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7((REAL 1),(REAL 1)) is set
K6(K7((REAL 1),(REAL 1))) is set
REAL-NS 1 is non empty V50() V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
the carrier of (REAL-NS 1) is non empty V2() set
R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)) is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V109() V142() L15()
BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)) is non empty Element of K6( 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 V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V204() RLSStruct
LinearOperators ((REAL-NS 1),(REAL-NS 1)) is non empty functional Element of K6( the carrier of K279( the carrier of (REAL-NS 1),(REAL-NS 1)))
K279( the carrier of (REAL-NS 1),(REAL-NS 1)) is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V204() RLSStruct
K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) is non empty functional 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 total V30( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) Element of K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))
0. (REAL-NS 1) is V52( REAL-NS 1) Element of the carrier of (REAL-NS 1)
the carrier of (REAL-NS 1) --> (0. (REAL-NS 1)) is non empty Relation-like the carrier of (REAL-NS 1) -defined the carrier of (REAL-NS 1) -valued Function-like total V30( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) Element of K6(K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))
K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) is set
K6(K7( 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 K7(K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)),K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) -defined K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) -valued Function-like total V30(K7(K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)),K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) Element of K6(K7(K7(K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)),K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))))
K7(K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)),K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) is set
K7(K7(K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)),K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) is set
K6(K7(K7(K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)),K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K123( 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 K7(REAL,K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) -defined K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) -valued Function-like total V30(K7(REAL,K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) Element of K6(K7(K7(REAL,K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))))
K7(REAL,K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) is V33() set
K7(K7(REAL,K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))) is V33() set
K6(K7(K7(REAL,K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),K123( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))) is V33() set
RLSStruct(# K123( 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 K279( the carrier of (REAL-NS 1),(REAL-NS 1)) is non empty set
K6( the carrier of K279( the carrier of (REAL-NS 1),(REAL-NS 1))) is set
K199(K279( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Element of LinearOperators ((REAL-NS 1),(REAL-NS 1))
K197(K279( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Relation-like K7((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 total V30(K7((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))), LinearOperators ((REAL-NS 1),(REAL-NS 1))) Element of K6(K7(K7((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))))
K7((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K7(K7((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K6(K7(K7((LinearOperators ((REAL-NS 1),(REAL-NS 1))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1))))) is set
K198(K279( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Relation-like K7(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) -defined LinearOperators ((REAL-NS 1),(REAL-NS 1)) -valued Function-like total V30(K7(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))), LinearOperators ((REAL-NS 1),(REAL-NS 1))) Element of K6(K7(K7(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))))
K7(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is V33() set
K7(K7(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is V33() set
K6(K7(K7(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1))))) is V33() set
RLSStruct(# (LinearOperators ((REAL-NS 1),(REAL-NS 1))),K199(K279( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),K197(K279( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),K198(K279( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) #) is V71() 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
K6( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K199((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))
K197((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Relation-like K7((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 total V30(K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))), BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) Element of K6(K7(K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))))
K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K7(K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K6(K7(K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))))) is set
K198((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Relation-like K7(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) -defined BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)) -valued Function-like total V30(K7(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))), BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) Element of K6(K7(K7(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))))
K7(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is V33() set
K7(K7(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is V33() set
K6(K7(K7(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))))) is V33() set
BoundedLinearOperatorsNorm ((REAL-NS 1),(REAL-NS 1)) is non empty Relation-like BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)) -defined REAL -valued Function-like total V30( BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)), REAL ) complex-yielding V146() V147() Element of K6(K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),REAL))
K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),REAL) is V33() complex-yielding V146() V147() set
K6(K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),REAL)) is V33() set
G15((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),K199((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),K197((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),K198((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 V108() L15()
the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) is non empty set
K7(COMPLEX,COMPLEX) is V33() complex-yielding set
K6(K7(COMPLEX,COMPLEX)) is V33() set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V33() complex-yielding set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is V33() set
K7(RAT,RAT) is RAT -valued V33() complex-yielding V146() V147() set
K6(K7(RAT,RAT)) is V33() set
K7(K7(RAT,RAT),RAT) is RAT -valued V33() complex-yielding V146() V147() set
K6(K7(K7(RAT,RAT),RAT)) is V33() set
K7(INT,INT) is RAT -valued INT -valued V33() complex-yielding V146() V147() set
K6(K7(INT,INT)) is V33() set
K7(K7(INT,INT),INT) is RAT -valued INT -valued V33() complex-yielding V146() V147() set
K6(K7(K7(INT,INT),INT)) is V33() set
K7(NAT,NAT) is RAT -valued INT -valued complex-yielding V146() V147() V148() set
K7(K7(NAT,NAT),NAT) is RAT -valued INT -valued complex-yielding V146() V147() V148() set
K6(K7(K7(NAT,NAT),NAT)) is set
K537() is non empty V73() L8()
the carrier of K537() is non empty set
K542() is non empty L8()
K543() is non empty V73() M15(K542())
K544() is non empty V73() V121() V220() M18(K542(),K543())
K546() is non empty V73() V121() V123() V125() L8()
K547() is non empty V73() V121() V220() M15(K546())
ExtREAL is non empty V157() set
{} is empty V6() functional V38() V40( {} ) V156() V157() V158() V159() V160() V161() V162() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered set
{{},1} is non empty set
K271() is V94() L11()
the carrier of K271() is set
the carrier of K271() * is functional FinSequence-membered FinSequenceSet of the carrier of K271()
TOP-REAL 1 is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V198() V205() L20()
the carrier of (TOP-REAL 1) is non empty set
0 is empty V6() V10() V11() V12() ext-real non positive non negative functional V33() V38() V40( {} ) V120() V155() V156() V157() V158() V159() V160() V161() V162() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered Element of NAT
- 1 is V11() V12() ext-real non positive Element of REAL
sqrreal is non empty Relation-like REAL -defined REAL -valued Function-like total V30( REAL , REAL ) complex-yielding V146() V147() Element of K6(K7(REAL,REAL))
<*> REAL is Relation-like NAT -defined REAL -valued Function-like FinSequence-like complex-yielding V146() V147() FinSequence of REAL
Sum (<*> REAL) is V11() V12() ext-real Element of REAL
proj (1,1) is non empty Relation-like REAL 1 -defined REAL -valued Function-like total V30( REAL 1, REAL ) complex-yielding V146() V147() Element of K6(K7((REAL 1),REAL))
K7((REAL 1),REAL) is V33() complex-yielding V146() V147() set
K6(K7((REAL 1),REAL)) is V33() set
(proj (1,1)) " is Relation-like Function-like set
m is V6() V10() V11() V12() ext-real non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL m is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL-NS m is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
the carrier of (REAL-NS m) is non empty set
n is V6() V10() V11() V12() ext-real non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7((REAL m),(REAL n)) is set
K6(K7((REAL m),(REAL n))) is set
REAL-NS n is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
the carrier of (REAL-NS n) is non empty set
K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) is set
K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is set
f is set
n is non empty V6() V10() V11() V12() ext-real positive non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
m is non empty V6() V10() V11() V12() ext-real positive non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL m is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7((REAL n),(REAL m)) is set
K6(K7((REAL n),(REAL m))) is set
REAL-NS n is non empty V50() V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
the carrier of (REAL-NS n) is non empty V2() set
REAL-NS m is non empty V50() V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
the carrier of (REAL-NS m) is non empty V2() set
K7( the carrier of (REAL-NS n), the carrier of (REAL-NS m)) is set
K6(K7( the carrier of (REAL-NS n), the carrier of (REAL-NS m))) is set
f is Relation-like REAL n -defined REAL m -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL n),(REAL m)))
Z is Relation-like the carrier of (REAL-NS n) -defined the carrier of (REAL-NS m) -valued Function-like Element of K6(K7( the carrier of (REAL-NS n), the carrier of (REAL-NS m)))
g is Relation-like NAT -defined REAL -valued Function-like V40(n) FinSequence-like complex-yielding V146() V147() Element of REAL n
Z0 is Element of the carrier of (REAL-NS n)
c7 is Relation-like the carrier of (REAL-NS n) -defined the carrier of (REAL-NS m) -valued Function-like Element of K6(K7( the carrier of (REAL-NS n), the carrier of (REAL-NS m)))
x is Element of the carrier of (REAL-NS n)
n is non empty V6() V10() V11() V12() ext-real positive non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
m is non empty V6() V10() V11() V12() ext-real positive non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL m is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7((REAL n),(REAL m)) is set
K6(K7((REAL n),(REAL m))) is set
REAL-NS n is non empty V50() V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
the carrier of (REAL-NS n) is non empty V2() set
REAL-NS m is non empty V50() V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
the carrier of (REAL-NS m) is non empty V2() set
K7( the carrier of (REAL-NS n), the carrier of (REAL-NS m)) is set
K6(K7( the carrier of (REAL-NS n), the carrier of (REAL-NS m))) is set
f is Relation-like REAL n -defined REAL m -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL n),(REAL m)))
Z is Relation-like the carrier of (REAL-NS n) -defined the carrier of (REAL-NS m) -valued Function-like Element of K6(K7( the carrier of (REAL-NS n), the carrier of (REAL-NS m)))
g is Relation-like NAT -defined REAL -valued Function-like V40(n) FinSequence-like complex-yielding V146() V147() Element of REAL n
diff (f,g) is non empty Relation-like REAL n -defined REAL m -valued Function-like total V30( REAL n, REAL m) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL n),(REAL m)))
Z0 is Element of the carrier of (REAL-NS n)
diff (Z,Z0) is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))
R_NormSpace_of_BoundedLinearOperators ((REAL-NS n),(REAL-NS m)) is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V109() V142() L15()
BoundedLinearOperators ((REAL-NS n),(REAL-NS m)) is non empty Element of K6( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS n),(REAL-NS m))))
R_VectorSpace_of_LinearOperators ((REAL-NS n),(REAL-NS m)) is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V204() RLSStruct
LinearOperators ((REAL-NS n),(REAL-NS m)) is non empty functional Element of K6( the carrier of K279( the carrier of (REAL-NS n),(REAL-NS m)))
K279( the carrier of (REAL-NS n),(REAL-NS m)) is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V204() RLSStruct
K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m)) is non empty functional M4( the carrier of (REAL-NS n), the carrier of (REAL-NS m))
FuncZero ( the carrier of (REAL-NS n),(REAL-NS m)) is Relation-like the carrier of (REAL-NS n) -defined the carrier of (REAL-NS m) -valued Function-like total V30( the carrier of (REAL-NS n), the carrier of (REAL-NS m)) Element of K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))
0. (REAL-NS m) is V52( REAL-NS m) Element of the carrier of (REAL-NS m)
the carrier of (REAL-NS n) --> (0. (REAL-NS m)) is non empty Relation-like the carrier of (REAL-NS n) -defined the carrier of (REAL-NS m) -valued Function-like total V30( the carrier of (REAL-NS n), the carrier of (REAL-NS m)) Element of K6(K7( the carrier of (REAL-NS n), the carrier of (REAL-NS m)))
FuncAdd ( the carrier of (REAL-NS n),(REAL-NS m)) is Relation-like K7(K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m)),K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))) -defined K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m)) -valued Function-like total V30(K7(K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m)),K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))),K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))) Element of K6(K7(K7(K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m)),K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))),K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))))
K7(K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m)),K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))) is set
K7(K7(K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m)),K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))),K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))) is set
K6(K7(K7(K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m)),K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))),K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m)))) is set
FuncExtMult ( the carrier of (REAL-NS n),(REAL-NS m)) is Relation-like K7(REAL,K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))) -defined K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m)) -valued Function-like total V30(K7(REAL,K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))),K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))) Element of K6(K7(K7(REAL,K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))),K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))))
K7(REAL,K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))) is V33() set
K7(K7(REAL,K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))),K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))) is V33() set
K6(K7(K7(REAL,K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m))),K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m)))) is V33() set
RLSStruct(# K123( the carrier of (REAL-NS n), the carrier of (REAL-NS m)),(FuncZero ( the carrier of (REAL-NS n),(REAL-NS m))),(FuncAdd ( the carrier of (REAL-NS n),(REAL-NS m))),(FuncExtMult ( the carrier of (REAL-NS n),(REAL-NS m))) #) is strict RLSStruct
the carrier of K279( the carrier of (REAL-NS n),(REAL-NS m)) is non empty set
K6( the carrier of K279( the carrier of (REAL-NS n),(REAL-NS m))) is set
K199(K279( the carrier of (REAL-NS n),(REAL-NS m)),(LinearOperators ((REAL-NS n),(REAL-NS m)))) is Element of LinearOperators ((REAL-NS n),(REAL-NS m))
K197(K279( the carrier of (REAL-NS n),(REAL-NS m)),(LinearOperators ((REAL-NS n),(REAL-NS m)))) is Relation-like K7((LinearOperators ((REAL-NS n),(REAL-NS m))),(LinearOperators ((REAL-NS n),(REAL-NS m)))) -defined LinearOperators ((REAL-NS n),(REAL-NS m)) -valued Function-like total V30(K7((LinearOperators ((REAL-NS n),(REAL-NS m))),(LinearOperators ((REAL-NS n),(REAL-NS m)))), LinearOperators ((REAL-NS n),(REAL-NS m))) Element of K6(K7(K7((LinearOperators ((REAL-NS n),(REAL-NS m))),(LinearOperators ((REAL-NS n),(REAL-NS m)))),(LinearOperators ((REAL-NS n),(REAL-NS m)))))
K7((LinearOperators ((REAL-NS n),(REAL-NS m))),(LinearOperators ((REAL-NS n),(REAL-NS m)))) is set
K7(K7((LinearOperators ((REAL-NS n),(REAL-NS m))),(LinearOperators ((REAL-NS n),(REAL-NS m)))),(LinearOperators ((REAL-NS n),(REAL-NS m)))) is set
K6(K7(K7((LinearOperators ((REAL-NS n),(REAL-NS m))),(LinearOperators ((REAL-NS n),(REAL-NS m)))),(LinearOperators ((REAL-NS n),(REAL-NS m))))) is set
K198(K279( the carrier of (REAL-NS n),(REAL-NS m)),(LinearOperators ((REAL-NS n),(REAL-NS m)))) is Relation-like K7(REAL,(LinearOperators ((REAL-NS n),(REAL-NS m)))) -defined LinearOperators ((REAL-NS n),(REAL-NS m)) -valued Function-like total V30(K7(REAL,(LinearOperators ((REAL-NS n),(REAL-NS m)))), LinearOperators ((REAL-NS n),(REAL-NS m))) Element of K6(K7(K7(REAL,(LinearOperators ((REAL-NS n),(REAL-NS m)))),(LinearOperators ((REAL-NS n),(REAL-NS m)))))
K7(REAL,(LinearOperators ((REAL-NS n),(REAL-NS m)))) is V33() set
K7(K7(REAL,(LinearOperators ((REAL-NS n),(REAL-NS m)))),(LinearOperators ((REAL-NS n),(REAL-NS m)))) is V33() set
K6(K7(K7(REAL,(LinearOperators ((REAL-NS n),(REAL-NS m)))),(LinearOperators ((REAL-NS n),(REAL-NS m))))) is V33() set
RLSStruct(# (LinearOperators ((REAL-NS n),(REAL-NS m))),K199(K279( the carrier of (REAL-NS n),(REAL-NS m)),(LinearOperators ((REAL-NS n),(REAL-NS m)))),K197(K279( the carrier of (REAL-NS n),(REAL-NS m)),(LinearOperators ((REAL-NS n),(REAL-NS m)))),K198(K279( the carrier of (REAL-NS n),(REAL-NS m)),(LinearOperators ((REAL-NS n),(REAL-NS m)))) #) is V71() 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 m))) is non empty set
K6( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS n),(REAL-NS m)))) is set
K199((R_VectorSpace_of_LinearOperators ((REAL-NS n),(REAL-NS m))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))) is Element of BoundedLinearOperators ((REAL-NS n),(REAL-NS m))
K197((R_VectorSpace_of_LinearOperators ((REAL-NS n),(REAL-NS m))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))) is Relation-like K7((BoundedLinearOperators ((REAL-NS n),(REAL-NS m))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))) -defined BoundedLinearOperators ((REAL-NS n),(REAL-NS m)) -valued Function-like total V30(K7((BoundedLinearOperators ((REAL-NS n),(REAL-NS m))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))), BoundedLinearOperators ((REAL-NS n),(REAL-NS m))) Element of K6(K7(K7((BoundedLinearOperators ((REAL-NS n),(REAL-NS m))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))))
K7((BoundedLinearOperators ((REAL-NS n),(REAL-NS m))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))) is set
K7(K7((BoundedLinearOperators ((REAL-NS n),(REAL-NS m))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))) is set
K6(K7(K7((BoundedLinearOperators ((REAL-NS n),(REAL-NS m))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m))))) is set
K198((R_VectorSpace_of_LinearOperators ((REAL-NS n),(REAL-NS m))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))) is Relation-like K7(REAL,(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))) -defined BoundedLinearOperators ((REAL-NS n),(REAL-NS m)) -valued Function-like total V30(K7(REAL,(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))), BoundedLinearOperators ((REAL-NS n),(REAL-NS m))) Element of K6(K7(K7(REAL,(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))))
K7(REAL,(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))) is V33() set
K7(K7(REAL,(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))) is V33() set
K6(K7(K7(REAL,(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m))))) is V33() set
BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS m)) is non empty Relation-like BoundedLinearOperators ((REAL-NS n),(REAL-NS m)) -defined REAL -valued Function-like total V30( BoundedLinearOperators ((REAL-NS n),(REAL-NS m)), REAL ) complex-yielding V146() V147() Element of K6(K7((BoundedLinearOperators ((REAL-NS n),(REAL-NS m))),REAL))
K7((BoundedLinearOperators ((REAL-NS n),(REAL-NS m))),REAL) is V33() complex-yielding V146() V147() set
K6(K7((BoundedLinearOperators ((REAL-NS n),(REAL-NS m))),REAL)) is V33() set
G15((BoundedLinearOperators ((REAL-NS n),(REAL-NS m))),K199((R_VectorSpace_of_LinearOperators ((REAL-NS n),(REAL-NS m))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))),K197((R_VectorSpace_of_LinearOperators ((REAL-NS n),(REAL-NS m))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))),K198((R_VectorSpace_of_LinearOperators ((REAL-NS n),(REAL-NS m))),(BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))),(BoundedLinearOperatorsNorm ((REAL-NS n),(REAL-NS m)))) is V108() L15()
the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS n),(REAL-NS m))) is non empty set
c7 is Relation-like the carrier of (REAL-NS n) -defined the carrier of (REAL-NS m) -valued Function-like Element of K6(K7( the carrier of (REAL-NS n), the carrier of (REAL-NS m)))
x is Element of the carrier of (REAL-NS n)
diff (c7,x) is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS n),(REAL-NS m)))
m is V6() V10() V11() V12() ext-real non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL m is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL-NS m is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
the carrier of (REAL-NS m) is non empty set
n is V6() V10() V11() V12() ext-real non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7((REAL m),(REAL n)) is set
K6(K7((REAL m),(REAL n))) is set
REAL-NS n is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
the carrier of (REAL-NS n) is non empty set
K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) is set
K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is set
f is Relation-like REAL m -defined REAL n -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
Z is Relation-like REAL m -defined REAL n -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
f + Z is Relation-like REAL m -defined REAL n -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
g is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))
Z0 is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))
g + Z0 is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))
dom f is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
K6((REAL m)) is set
dom Z is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
(dom f) /\ (dom Z) is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
c7 is Relation-like REAL m -defined REAL n -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
dom c7 is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
f <++> Z is Relation-like (REAL m) /\ (REAL m) -defined R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))) -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(((REAL m) /\ (REAL m)),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))))
(REAL m) /\ (REAL m) is set
DOMS (REAL n) is set
(DOMS (REAL n)) /\ (DOMS (REAL n)) is set
R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
K7(((REAL m) /\ (REAL m)),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))) is set
K6(K7(((REAL m) /\ (REAL m)),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))))) is set
x is set
(g + Z0) . x is set
f . x is Relation-like Function-like complex-yielding V146() V147() set
Z . x is Relation-like Function-like complex-yielding V146() V147() set
(f . x) + (Z . x) is Relation-like Function-like set
dom (g + Z0) is Element of K6( the carrier of (REAL-NS m))
K6( the carrier of (REAL-NS m)) is set
f /. x is V40(n) complex-yielding V146() V147() Element of REAL n
Z /. x is V40(n) complex-yielding V146() V147() Element of REAL n
g /. x is Element of the carrier of (REAL-NS n)
Z0 /. x is Element of the carrier of (REAL-NS n)
c7 . x is Relation-like Function-like complex-yielding V146() V147() set
(g + Z0) /. x is Element of the carrier of (REAL-NS n)
(g /. x) + (Z0 /. x) is Element of the carrier of (REAL-NS n)
m is V6() V10() V11() V12() ext-real non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL m is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL-NS m is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
the carrier of (REAL-NS m) is non empty set
n is V6() V10() V11() V12() ext-real non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7((REAL m),(REAL n)) is set
K6(K7((REAL m),(REAL n))) is set
REAL-NS n is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
the carrier of (REAL-NS n) is non empty set
K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) is set
K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is set
f is Relation-like REAL m -defined REAL n -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
Z is Relation-like REAL m -defined REAL n -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
f - Z is Relation-like REAL m -defined REAL n -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
g is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))
Z0 is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))
g - Z0 is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))
dom f is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
K6((REAL m)) is set
dom Z is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
(dom f) /\ (dom Z) is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
c7 is Relation-like REAL m -defined REAL n -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
dom c7 is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
f <--> Z is Relation-like (REAL m) /\ (REAL m) -defined R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))) -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(((REAL m) /\ (REAL m)),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))))
(REAL m) /\ (REAL m) is set
DOMS (REAL n) is set
(DOMS (REAL n)) /\ (DOMS (REAL n)) is set
R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
K7(((REAL m) /\ (REAL m)),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))) is set
K6(K7(((REAL m) /\ (REAL m)),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))))) is set
x is set
(g - Z0) . x is set
f . x is Relation-like Function-like complex-yielding V146() V147() set
Z . x is Relation-like Function-like complex-yielding V146() V147() set
(f . x) - (Z . x) is Relation-like Function-like set
- (Z . x) is Relation-like Function-like complex-yielding set
- 1 is V11() V12() ext-real non positive set
(- 1) (#) (Z . x) is Relation-like Function-like set
(f . x) + (- (Z . x)) is Relation-like Function-like set
dom (g - Z0) is Element of K6( the carrier of (REAL-NS m))
K6( the carrier of (REAL-NS m)) is set
f /. x is V40(n) complex-yielding V146() V147() Element of REAL n
Z /. x is V40(n) complex-yielding V146() V147() Element of REAL n
g /. x is Element of the carrier of (REAL-NS n)
Z0 /. x is Element of the carrier of (REAL-NS n)
c7 . x is Relation-like Function-like complex-yielding V146() V147() set
(g - Z0) /. x is Element of the carrier of (REAL-NS n)
(g /. x) - (Z0 /. x) is Element of the carrier of (REAL-NS n)
m is V6() V10() V11() V12() ext-real non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL m is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL-NS m is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
the carrier of (REAL-NS m) is non empty set
n is V6() V10() V11() V12() ext-real non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7((REAL m),(REAL n)) is set
K6(K7((REAL m),(REAL n))) is set
REAL-NS n is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
the carrier of (REAL-NS n) is non empty set
K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) is set
K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is set
f is Relation-like REAL m -defined REAL n -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
Z is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))
g is V11() V12() ext-real Element of REAL
g (#) f is Relation-like REAL m -defined REAL n -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
g (#) Z is Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))
dom f is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
K6((REAL m)) is set
Z0 is Relation-like REAL m -defined REAL n -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
dom Z0 is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
f [#] g is Relation-like REAL m -defined R_PFuncs (DOMS (REAL n)) -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(R_PFuncs (DOMS (REAL n)))))
DOMS (REAL n) is set
R_PFuncs (DOMS (REAL n)) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
K7((REAL m),(R_PFuncs (DOMS (REAL n)))) is set
K6(K7((REAL m),(R_PFuncs (DOMS (REAL n))))) is set
c7 is set
Z0 . c7 is Relation-like Function-like complex-yielding V146() V147() set
f . c7 is Relation-like Function-like complex-yielding V146() V147() set
g (#) (f . c7) is Relation-like Function-like set
dom (g (#) Z) is Element of K6( the carrier of (REAL-NS m))
K6( the carrier of (REAL-NS m)) is set
f /. c7 is V40(n) complex-yielding V146() V147() Element of REAL n
Z /. c7 is Element of the carrier of (REAL-NS n)
(g (#) Z) /. c7 is Element of the carrier of (REAL-NS n)
g * (Z /. c7) is Element of the carrier of (REAL-NS n)
m is V6() V10() V11() V12() ext-real non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL m is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL-NS m is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
n is V6() V10() V11() V12() ext-real non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7((REAL m),(REAL n)) is set
K6(K7((REAL m),(REAL n))) is set
REAL-NS n is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V109() V142() L15()
BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) is non empty Element of K6( 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 V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V204() RLSStruct
LinearOperators ((REAL-NS m),(REAL-NS n)) is non empty functional Element of K6( the carrier of K279( the carrier of (REAL-NS m),(REAL-NS n)))
the carrier of (REAL-NS m) is non empty set
K279( the carrier of (REAL-NS m),(REAL-NS n)) is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V204() RLSStruct
the carrier of (REAL-NS n) is non empty set
K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) is non empty functional 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 total V30( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) Element of K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))
0. (REAL-NS n) is V52( REAL-NS n) Element of the carrier of (REAL-NS n)
the carrier of (REAL-NS m) --> (0. (REAL-NS n)) is non empty Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS n) -valued Function-like total V30( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) Element of K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))
K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) is set
K6(K7( 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 K7(K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) -defined K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) -valued Function-like total V30(K7(K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) Element of K6(K7(K7(K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))))
K7(K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is set
K7(K7(K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is set
K6(K7(K7(K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( 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 K7(REAL,K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) -defined K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) -valued Function-like total V30(K7(REAL,K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) Element of K6(K7(K7(REAL,K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))))
K7(REAL,K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is V33() set
K7(K7(REAL,K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is V33() set
K6(K7(K7(REAL,K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))) is V33() set
RLSStruct(# K123( 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 K279( the carrier of (REAL-NS m),(REAL-NS n)) is non empty set
K6( the carrier of K279( the carrier of (REAL-NS m),(REAL-NS n))) is set
K199(K279( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is Element of LinearOperators ((REAL-NS m),(REAL-NS n))
K197(K279( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K7((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 total V30(K7((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))), LinearOperators ((REAL-NS m),(REAL-NS n))) Element of K6(K7(K7((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))))
K7((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is set
K7(K7((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is set
K6(K7(K7((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n))))) is set
K198(K279( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K7(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))) -defined LinearOperators ((REAL-NS m),(REAL-NS n)) -valued Function-like total V30(K7(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))), LinearOperators ((REAL-NS m),(REAL-NS n))) Element of K6(K7(K7(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))))
K7(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))) is V33() set
K7(K7(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is V33() set
K6(K7(K7(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n))))) is V33() set
RLSStruct(# (LinearOperators ((REAL-NS m),(REAL-NS n))),K199(K279( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))),K197(K279( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))),K198(K279( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) #) is V71() 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
K6( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n)))) is set
K199((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))
K197((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K7((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 total V30(K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))), BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) Element of K6(K7(K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))))
K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is set
K7(K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is set
K6(K7(K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n))))) is set
K198((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K7(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) -defined BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) -valued Function-like total V30(K7(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))), BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) Element of K6(K7(K7(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))))
K7(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is V33() set
K7(K7(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is V33() set
K6(K7(K7(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n))))) is V33() set
BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS n)) is non empty Relation-like BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) -defined REAL -valued Function-like total V30( BoundedLinearOperators ((REAL-NS m),(REAL-NS n)), REAL ) complex-yielding V146() V147() Element of K6(K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),REAL))
K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),REAL) is V33() complex-yielding V146() V147() set
K6(K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),REAL)) is V33() set
G15((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),K199((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),K197((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),K198((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 V108() L15()
the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) is non empty set
f is non empty Relation-like REAL m -defined REAL n -valued Function-like total V30( REAL m, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
Z is non empty Relation-like REAL m -defined REAL n -valued Function-like total V30( REAL m, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
f + Z is Relation-like REAL m -defined REAL n -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
g is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
Z0 is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
g + Z0 is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
dom g is set
dom Z0 is set
dom f is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
K6((REAL m)) is set
dom Z is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
(dom f) /\ (dom Z) is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
c7 is non empty Relation-like REAL m -defined REAL n -valued Function-like total V30( REAL m, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
dom c7 is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
f <++> Z is Relation-like (REAL m) /\ (REAL m) -defined R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))) -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(((REAL m) /\ (REAL m)),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))))
(REAL m) /\ (REAL m) is set
DOMS (REAL n) is set
(DOMS (REAL n)) /\ (DOMS (REAL n)) is set
R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
K7(((REAL m) /\ (REAL m)),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))) is set
K6(K7(((REAL m) /\ (REAL m)),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))))) is set
x is set
c7 . x is Relation-like Function-like complex-yielding V146() V147() set
f . x is Relation-like Function-like complex-yielding V146() V147() set
Z . x is Relation-like Function-like complex-yielding V146() V147() set
(f . x) + (Z . x) is Relation-like Function-like set
L is Element of the carrier of (REAL-NS m)
c7 . L is Relation-like Function-like complex-yielding V146() V147() set
g . L is Element of the carrier of (REAL-NS n)
Z0 . L is Element of the carrier of (REAL-NS n)
(g . L) + (Z0 . L) is Element of the carrier of (REAL-NS n)
L0 is Relation-like NAT -defined REAL -valued Function-like V40(m) FinSequence-like complex-yielding V146() V147() Element of REAL m
f /. L0 is V40(n) complex-yielding V146() V147() Element of REAL n
f . L0 is Relation-like Function-like V40(n) complex-yielding V146() V147() Element of REAL n
Z /. L0 is V40(n) complex-yielding V146() V147() Element of REAL n
Z . L0 is Relation-like Function-like V40(n) complex-yielding V146() V147() Element of REAL n
(f /. L0) + (Z /. L0) is Relation-like NAT -defined REAL -valued Function-like V40(n) FinSequence-like complex-yielding V146() V147() Element of REAL n
m is V6() V10() V11() V12() ext-real non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL m is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
REAL-NS m is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
n is V6() V10() V11() V12() ext-real non negative V33() V38() V120() V155() V156() V157() V158() V159() V160() V161() Element of NAT
REAL n is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7((REAL m),(REAL n)) is set
K6(K7((REAL m),(REAL n))) is set
REAL-NS n is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V108() V109() V142() L15()
R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() V109() V142() L15()
BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) is non empty Element of K6( 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 V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V204() RLSStruct
LinearOperators ((REAL-NS m),(REAL-NS n)) is non empty functional Element of K6( the carrier of K279( the carrier of (REAL-NS m),(REAL-NS n)))
the carrier of (REAL-NS m) is non empty set
K279( the carrier of (REAL-NS m),(REAL-NS n)) is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V204() RLSStruct
the carrier of (REAL-NS n) is non empty set
K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) is non empty functional 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 total V30( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) Element of K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))
0. (REAL-NS n) is V52( REAL-NS n) Element of the carrier of (REAL-NS n)
the carrier of (REAL-NS m) --> (0. (REAL-NS n)) is non empty Relation-like the carrier of (REAL-NS m) -defined the carrier of (REAL-NS n) -valued Function-like total V30( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) Element of K6(K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))
K7( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) is set
K6(K7( 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 K7(K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) -defined K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) -valued Function-like total V30(K7(K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) Element of K6(K7(K7(K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))))
K7(K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is set
K7(K7(K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is set
K6(K7(K7(K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( 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 K7(REAL,K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) -defined K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)) -valued Function-like total V30(K7(REAL,K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) Element of K6(K7(K7(REAL,K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))))
K7(REAL,K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is V33() set
K7(K7(REAL,K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))) is V33() set
K6(K7(K7(REAL,K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n))),K123( the carrier of (REAL-NS m), the carrier of (REAL-NS n)))) is V33() set
RLSStruct(# K123( 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 K279( the carrier of (REAL-NS m),(REAL-NS n)) is non empty set
K6( the carrier of K279( the carrier of (REAL-NS m),(REAL-NS n))) is set
K199(K279( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is Element of LinearOperators ((REAL-NS m),(REAL-NS n))
K197(K279( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K7((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 total V30(K7((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))), LinearOperators ((REAL-NS m),(REAL-NS n))) Element of K6(K7(K7((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))))
K7((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is set
K7(K7((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is set
K6(K7(K7((LinearOperators ((REAL-NS m),(REAL-NS n))),(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n))))) is set
K198(K279( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K7(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))) -defined LinearOperators ((REAL-NS m),(REAL-NS n)) -valued Function-like total V30(K7(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))), LinearOperators ((REAL-NS m),(REAL-NS n))) Element of K6(K7(K7(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))))
K7(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))) is V33() set
K7(K7(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n)))) is V33() set
K6(K7(K7(REAL,(LinearOperators ((REAL-NS m),(REAL-NS n)))),(LinearOperators ((REAL-NS m),(REAL-NS n))))) is V33() set
RLSStruct(# (LinearOperators ((REAL-NS m),(REAL-NS n))),K199(K279( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))),K197(K279( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))),K198(K279( the carrier of (REAL-NS m),(REAL-NS n)),(LinearOperators ((REAL-NS m),(REAL-NS n)))) #) is V71() 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
K6( the carrier of (R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n)))) is set
K199((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))
K197((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K7((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 total V30(K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))), BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) Element of K6(K7(K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))))
K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is set
K7(K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is set
K6(K7(K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n))))) is set
K198((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is Relation-like K7(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) -defined BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) -valued Function-like total V30(K7(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))), BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) Element of K6(K7(K7(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))))
K7(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is V33() set
K7(K7(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))) is V33() set
K6(K7(K7(REAL,(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n))))) is V33() set
BoundedLinearOperatorsNorm ((REAL-NS m),(REAL-NS n)) is non empty Relation-like BoundedLinearOperators ((REAL-NS m),(REAL-NS n)) -defined REAL -valued Function-like total V30( BoundedLinearOperators ((REAL-NS m),(REAL-NS n)), REAL ) complex-yielding V146() V147() Element of K6(K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),REAL))
K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),REAL) is V33() complex-yielding V146() V147() set
K6(K7((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),REAL)) is V33() set
G15((BoundedLinearOperators ((REAL-NS m),(REAL-NS n))),K199((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),K197((R_VectorSpace_of_LinearOperators ((REAL-NS m),(REAL-NS n))),(BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))),K198((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 V108() L15()
the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) is non empty set
f is non empty Relation-like REAL m -defined REAL n -valued Function-like total V30( REAL m, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
Z is non empty Relation-like REAL m -defined REAL n -valued Function-like total V30( REAL m, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
f - Z is Relation-like REAL m -defined REAL n -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
g is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
Z0 is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
g - Z0 is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
dom g is set
dom Z0 is set
dom f is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
K6((REAL m)) is set
dom Z is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
(dom f) /\ (dom Z) is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
c7 is non empty Relation-like REAL m -defined REAL n -valued Function-like total V30( REAL m, REAL n) complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7((REAL m),(REAL n)))
dom c7 is functional complex-functions-membered ext-real-functions-membered real-functions-membered Element of K6((REAL m))
f <--> Z is Relation-like (REAL m) /\ (REAL m) -defined R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))) -valued Function-like complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(((REAL m) /\ (REAL m)),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))))
(REAL m) /\ (REAL m) is set
DOMS (REAL n) is set
(DOMS (REAL n)) /\ (DOMS (REAL n)) is set
R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
K7(((REAL m) /\ (REAL m)),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n))))) is set
K6(K7(((REAL m) /\ (REAL m)),(R_PFuncs ((DOMS (REAL n)) /\ (DOMS (REAL n)))))) is set
x is set
c7 . x is Relation-like Function-like complex-yielding V146() V147() set
f . x is Relation-like Function-like complex-yielding V146() V147() set
Z . x is Relation-like Function-like complex-yielding V146() V147() set
(f . x) - (Z . x) is Relation-like Function-like set
- (Z . x) is Relation-like Function-like complex-yielding set
- 1 is V11() V12() ext-real non positive set
(- 1) (#) (Z . x) is Relation-like Function-like set
(f . x) + (- (Z . x)) is Relation-like Function-like set
L is Element of the carrier of (REAL-NS m)
c7 . L is Relation-like Function-like complex-yielding V146() V147() set
g . L is Element of the carrier of (REAL-NS n)
Z0 . L is Element of the carrier of (REAL-NS n)
(g . L) - (Z0 . L) is Element of the carrier of (REAL-NS n)
L0 is Relation-like NAT -defined REAL -valued Function-like V40(m) FinSequence-like complex-yielding V146() V147() Element of REAL m
f /. L0 is V40(n) complex-yielding V146() V147() Element of REAL n
f . L0 is Relation-like Function-like V40(n) complex-yielding V146() V147() Element of REAL n
Z /. L0 is V40(n) complex-yielding V146() V147() Element of REAL n
Z . L0 is Relation-like Function-like V40(n) complex-yielding V146() V147() Element of REAL n
(f /. L0) - (Z /. L0) is Relation-like NAT -defined REAL -valued Function-like V40(n) FinSequence-like complex-yielding V146() V147() Element of REAL n
m is