:: PDIFF_6 semantic presentation

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)

c

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

c

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

diff (c

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

c

dom c

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)

c

(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))

c

dom c

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)

c

(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

c

Z0 . c

f . c

g (#) (f . c

dom (g (#) Z) is Element of K6( the carrier of (REAL-NS m))

K6( the carrier of (REAL-NS m)) is set

f /. c

Z /. c

(g (#) Z) /. c

g * (Z /. c

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

c

dom c

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

c

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)

c

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

c

dom c

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

c

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)

c

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