REAL is non empty V33() V196() V197() V198() V202() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V196() V197() V198() V199() V200() V201() V202() Element of K6(REAL)
K6(REAL) is set
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(NAT,(REAL *)) is set
K6(K7(NAT,(REAL *))) is set
COMPLEX is non empty V33() V196() V202() set
omega is non empty epsilon-transitive epsilon-connected ordinal V196() V197() V198() V199() V200() V201() V202() set
K6(omega) is set
K6(NAT) is set
K7(NAT,REAL) is complex-yielding V186() V187() set
K6(K7(NAT,REAL)) is 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 set
K7(K7(REAL,K190()),K190()) is set
K6(K7(K7(REAL,K190()),K190())) is 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 V186() V187() set
K6(K7(K7(K200(),K200()),REAL)) is set
K203() is Element of K6( the carrier of K196())
K7(K203(),REAL) is complex-yielding V186() V187() set
K6(K7(K203(),REAL)) is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
INT is non empty V33() V196() V197() V198() V199() V200() V202() set
K7(1,1) is RAT -valued INT -valued complex-yielding V186() V187() V188() set
RAT is non empty V33() V196() V197() V198() V199() V202() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is RAT -valued INT -valued complex-yielding V186() V187() V188() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is complex-yielding V186() V187() set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is complex-yielding V186() V187() set
K7(K7(REAL,REAL),REAL) is complex-yielding V186() V187() set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
K7(2,2) is RAT -valued INT -valued complex-yielding V186() V187() V188() set
K7(K7(2,2),REAL) is complex-yielding V186() V187() set
K6(K7(K7(2,2),REAL)) is set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V145() V209() L19()
the carrier of (TOP-REAL 2) is non empty set
REAL 1 is non empty functional FinSequence-membered V263() V264() V265() FinSequenceSet of REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = 1 } is set
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() strict RealNormSpace-like V182() NORMSTR
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() RealNormSpace-like V182() NORMSTR
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 V208() RLSStruct
LinearOperators ((REAL-NS 1),(REAL-NS 1)) is non empty functional Element of K6( the carrier of K310( the carrier of (REAL-NS 1),(REAL-NS 1)))
K310( 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 V208() RLSStruct
Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) is non empty functional FUNCTION_DOMAIN of 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 quasi_total Element of Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))
K153((REAL-NS 1)) is V52( REAL-NS 1) Element of the carrier of (REAL-NS 1)
K257( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1),K153((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 quasi_total 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((Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))) -defined Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) -valued Function-like total quasi_total Element of K6(K7(K7((Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))))
K7((Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))) is set
K7(K7((Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))) is set
K6(K7(K7((Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))),(Funcs ( 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,(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))) -defined Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)) -valued Function-like total quasi_total Element of K6(K7(K7(REAL,(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))))
K7(REAL,(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))) is set
K7(K7(REAL,(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))) is set
K6(K7(K7(REAL,(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1)))),(Funcs ( the carrier of (REAL-NS 1), the carrier of (REAL-NS 1))))) is set
RLSStruct(# (Funcs ( 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 K310( the carrier of (REAL-NS 1),(REAL-NS 1)) is non empty set
K6( the carrier of K310( the carrier of (REAL-NS 1),(REAL-NS 1))) is set
K199(K310( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is Relation-like Function-like Element of LinearOperators ((REAL-NS 1),(REAL-NS 1))
K197(K310( 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 quasi_total 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(K310( 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 quasi_total 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 set
K7(K7(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K6(K7(K7(REAL,(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),(LinearOperators ((REAL-NS 1),(REAL-NS 1))))) is set
RLSStruct(# (LinearOperators ((REAL-NS 1),(REAL-NS 1))),K199(K310( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),K197(K310( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),K198(K310( 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 quasi_total 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 quasi_total 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 set
K7(K7(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))) is set
K6(K7(K7(REAL,(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))))) is 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 quasi_total complex-yielding V186() V187() Element of K6(K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),REAL))
K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),REAL) is complex-yielding V186() V187() set
K6(K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),REAL)) is set
NORMSTR(# (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 strict NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))) is non empty set
K7(COMPLEX,COMPLEX) is complex-yielding set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is complex-yielding set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is RAT -valued complex-yielding V186() V187() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is RAT -valued complex-yielding V186() V187() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is RAT -valued INT -valued complex-yielding V186() V187() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is RAT -valued INT -valued complex-yielding V186() V187() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is RAT -valued INT -valued complex-yielding V186() V187() V188() set
K7(K7(NAT,NAT),NAT) is RAT -valued INT -valued complex-yielding V186() V187() V188() set
K6(K7(K7(NAT,NAT),NAT)) is set
K529() is non empty V73() L8()
the carrier of K529() is non empty set
K534() is non empty L8()
K535() is non empty V73() M17(K534())
K536() is non empty V73() V161() V224() M20(K534(),K535())
K538() is non empty V73() V161() V163() V165() L8()
K539() is non empty V73() V161() V224() M17(K538())
ExtREAL is non empty V197() set
K7(COMPLEX,REAL) is complex-yielding V186() V187() set
K6(K7(COMPLEX,REAL)) is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional FinSequence-membered V196() V197() V198() V199() V200() V201() V202() V263() V264() V265() V266() V267() V268() set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional FinSequence-membered V160() V195() V196() V197() V198() V199() V200() V201() V202() V263() V264() V265() V266() V267() V268() Element of NAT
Seg 1 is non empty V33() V40(1) V196() V197() V198() V199() V200() V201() Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
proj (1,1) is non empty Relation-like REAL 1 -defined REAL -valued Function-like total quasi_total complex-yielding V186() V187() Element of K6(K7((REAL 1),REAL))
K7((REAL 1),REAL) is complex-yielding V186() V187() set
K6(K7((REAL 1),REAL)) is set
(proj (1,1)) " is Relation-like Function-like set
K7(REAL,(REAL 1)) is set
K6(K7(REAL,(REAL 1))) is set
dom ((proj (1,1)) ") is set
rng ((proj (1,1)) ") is set
<*1*> is non empty Relation-like NAT -defined NAT -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() V188() FinSequence of NAT
[1,1] is set
{1,1} is non empty V196() V197() V198() V199() V200() V201() set
{1} is non empty V196() V197() V198() V199() V200() V201() set
{{1,1},{1}} is non empty set
{[1,1]} is non empty Function-like set
- 1 is non empty V11() real ext-real non positive negative Element of REAL
Z0 is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() RealNormSpace-like NORMSTR
m is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() RealNormSpace-like NORMSTR
R_NormSpace_of_BoundedLinearOperators (Z0,m) is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() RealNormSpace-like NORMSTR
BoundedLinearOperators (Z0,m) is non empty Element of K6( the carrier of (R_VectorSpace_of_LinearOperators (Z0,m)))
R_VectorSpace_of_LinearOperators (Z0,m) is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V208() RLSStruct
LinearOperators (Z0,m) is non empty functional Element of K6( the carrier of K310( the carrier of Z0,m))
the carrier of Z0 is non empty set
K310( the carrier of Z0,m) is non empty V71() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V208() RLSStruct
the carrier of m is non empty set
Funcs ( the carrier of Z0, the carrier of m) is non empty functional FUNCTION_DOMAIN of the carrier of Z0, the carrier of m
FuncZero ( the carrier of Z0,m) is Relation-like the carrier of Z0 -defined the carrier of m -valued Function-like total quasi_total Element of Funcs ( the carrier of Z0, the carrier of m)
K153(m) is V52(m) Element of the carrier of m
K257( the carrier of m, the carrier of Z0,K153(m)) is non empty Relation-like the carrier of Z0 -defined the carrier of m -valued Function-like total quasi_total Element of K6(K7( the carrier of Z0, the carrier of m))
K7( the carrier of Z0, the carrier of m) is set
K6(K7( the carrier of Z0, the carrier of m)) is set
FuncAdd ( the carrier of Z0,m) is Relation-like K7((Funcs ( the carrier of Z0, the carrier of m)),(Funcs ( the carrier of Z0, the carrier of m))) -defined Funcs ( the carrier of Z0, the carrier of m) -valued Function-like total quasi_total Element of K6(K7(K7((Funcs ( the carrier of Z0, the carrier of m)),(Funcs ( the carrier of Z0, the carrier of m))),(Funcs ( the carrier of Z0, the carrier of m))))
K7((Funcs ( the carrier of Z0, the carrier of m)),(Funcs ( the carrier of Z0, the carrier of m))) is set
K7(K7((Funcs ( the carrier of Z0, the carrier of m)),(Funcs ( the carrier of Z0, the carrier of m))),(Funcs ( the carrier of Z0, the carrier of m))) is set
K6(K7(K7((Funcs ( the carrier of Z0, the carrier of m)),(Funcs ( the carrier of Z0, the carrier of m))),(Funcs ( the carrier of Z0, the carrier of m)))) is set
FuncExtMult ( the carrier of Z0,m) is Relation-like K7(REAL,(Funcs ( the carrier of Z0, the carrier of m))) -defined Funcs ( the carrier of Z0, the carrier of m) -valued Function-like total quasi_total Element of K6(K7(K7(REAL,(Funcs ( the carrier of Z0, the carrier of m))),(Funcs ( the carrier of Z0, the carrier of m))))
K7(REAL,(Funcs ( the carrier of Z0, the carrier of m))) is set
K7(K7(REAL,(Funcs ( the carrier of Z0, the carrier of m))),(Funcs ( the carrier of Z0, the carrier of m))) is set
K6(K7(K7(REAL,(Funcs ( the carrier of Z0, the carrier of m))),(Funcs ( the carrier of Z0, the carrier of m)))) is set
RLSStruct(# (Funcs ( the carrier of Z0, the carrier of m)),(FuncZero ( the carrier of Z0,m)),(FuncAdd ( the carrier of Z0,m)),(FuncExtMult ( the carrier of Z0,m)) #) is strict RLSStruct
the carrier of K310( the carrier of Z0,m) is non empty set
K6( the carrier of K310( the carrier of Z0,m)) is set
K199(K310( the carrier of Z0,m),(LinearOperators (Z0,m))) is Relation-like Function-like Element of LinearOperators (Z0,m)
K197(K310( the carrier of Z0,m),(LinearOperators (Z0,m))) is Relation-like K7((LinearOperators (Z0,m)),(LinearOperators (Z0,m))) -defined LinearOperators (Z0,m) -valued Function-like total quasi_total Element of K6(K7(K7((LinearOperators (Z0,m)),(LinearOperators (Z0,m))),(LinearOperators (Z0,m))))
K7((LinearOperators (Z0,m)),(LinearOperators (Z0,m))) is set
K7(K7((LinearOperators (Z0,m)),(LinearOperators (Z0,m))),(LinearOperators (Z0,m))) is set
K6(K7(K7((LinearOperators (Z0,m)),(LinearOperators (Z0,m))),(LinearOperators (Z0,m)))) is set
K198(K310( the carrier of Z0,m),(LinearOperators (Z0,m))) is Relation-like K7(REAL,(LinearOperators (Z0,m))) -defined LinearOperators (Z0,m) -valued Function-like total quasi_total Element of K6(K7(K7(REAL,(LinearOperators (Z0,m))),(LinearOperators (Z0,m))))
K7(REAL,(LinearOperators (Z0,m))) is set
K7(K7(REAL,(LinearOperators (Z0,m))),(LinearOperators (Z0,m))) is set
K6(K7(K7(REAL,(LinearOperators (Z0,m))),(LinearOperators (Z0,m)))) is set
RLSStruct(# (LinearOperators (Z0,m)),K199(K310( the carrier of Z0,m),(LinearOperators (Z0,m))),K197(K310( the carrier of Z0,m),(LinearOperators (Z0,m))),K198(K310( the carrier of Z0,m),(LinearOperators (Z0,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 (Z0,m)) is non empty set
K6( the carrier of (R_VectorSpace_of_LinearOperators (Z0,m))) is set
K199((R_VectorSpace_of_LinearOperators (Z0,m)),(BoundedLinearOperators (Z0,m))) is Element of BoundedLinearOperators (Z0,m)
K197((R_VectorSpace_of_LinearOperators (Z0,m)),(BoundedLinearOperators (Z0,m))) is Relation-like K7((BoundedLinearOperators (Z0,m)),(BoundedLinearOperators (Z0,m))) -defined BoundedLinearOperators (Z0,m) -valued Function-like total quasi_total Element of K6(K7(K7((BoundedLinearOperators (Z0,m)),(BoundedLinearOperators (Z0,m))),(BoundedLinearOperators (Z0,m))))
K7((BoundedLinearOperators (Z0,m)),(BoundedLinearOperators (Z0,m))) is set
K7(K7((BoundedLinearOperators (Z0,m)),(BoundedLinearOperators (Z0,m))),(BoundedLinearOperators (Z0,m))) is set
K6(K7(K7((BoundedLinearOperators (Z0,m)),(BoundedLinearOperators (Z0,m))),(BoundedLinearOperators (Z0,m)))) is set
K198((R_VectorSpace_of_LinearOperators (Z0,m)),(BoundedLinearOperators (Z0,m))) is Relation-like K7(REAL,(BoundedLinearOperators (Z0,m))) -defined BoundedLinearOperators (Z0,m) -valued Function-like total quasi_total Element of K6(K7(K7(REAL,(BoundedLinearOperators (Z0,m))),(BoundedLinearOperators (Z0,m))))
K7(REAL,(BoundedLinearOperators (Z0,m))) is set
K7(K7(REAL,(BoundedLinearOperators (Z0,m))),(BoundedLinearOperators (Z0,m))) is set
K6(K7(K7(REAL,(BoundedLinearOperators (Z0,m))),(BoundedLinearOperators (Z0,m)))) is set
BoundedLinearOperatorsNorm (Z0,m) is non empty Relation-like BoundedLinearOperators (Z0,m) -defined REAL -valued Function-like total quasi_total complex-yielding V186() V187() Element of K6(K7((BoundedLinearOperators (Z0,m)),REAL))
K7((BoundedLinearOperators (Z0,m)),REAL) is complex-yielding V186() V187() set
K6(K7((BoundedLinearOperators (Z0,m)),REAL)) is set
NORMSTR(# (BoundedLinearOperators (Z0,m)),K199((R_VectorSpace_of_LinearOperators (Z0,m)),(BoundedLinearOperators (Z0,m))),K197((R_VectorSpace_of_LinearOperators (Z0,m)),(BoundedLinearOperators (Z0,m))),K198((R_VectorSpace_of_LinearOperators (Z0,m)),(BoundedLinearOperators (Z0,m))),(BoundedLinearOperatorsNorm (Z0,m)) #) is strict NORMSTR
the carrier of (R_NormSpace_of_BoundedLinearOperators (Z0,m)) is non empty set
Z is Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (Z0,m))
||.Z.|| is V11() real ext-real non negative Element of REAL
the U8 of (R_NormSpace_of_BoundedLinearOperators (Z0,m)) is non empty Relation-like the carrier of (R_NormSpace_of_BoundedLinearOperators (Z0,m)) -defined REAL -valued Function-like total quasi_total complex-yielding V186() V187() Element of K6(K7( the carrier of (R_NormSpace_of_BoundedLinearOperators (Z0,m)),REAL))
K7( the carrier of (R_NormSpace_of_BoundedLinearOperators (Z0,m)),REAL) is complex-yielding V186() V187() set
K6(K7( the carrier of (R_NormSpace_of_BoundedLinearOperators (Z0,m)),REAL)) is set
the U8 of (R_NormSpace_of_BoundedLinearOperators (Z0,m)) . Z is V11() real ext-real Element of REAL
k is V11() real ext-real Element of REAL
f is Element of the carrier of Z0
||.f.|| is V11() real ext-real non negative Element of REAL
the U8 of Z0 is non empty Relation-like the carrier of Z0 -defined REAL -valued Function-like total quasi_total complex-yielding V186() V187() Element of K6(K7( the carrier of Z0,REAL))
K7( the carrier of Z0,REAL) is complex-yielding V186() V187() set
K6(K7( the carrier of Z0,REAL)) is set
the U8 of Z0 . f is V11() real ext-real Element of REAL
Z . f is Element of the carrier of m
||.(Z . f).|| is V11() real ext-real non negative Element of REAL
the U8 of m is non empty Relation-like the carrier of m -defined REAL -valued Function-like total quasi_total complex-yielding V186() V187() Element of K6(K7( the carrier of m,REAL))
K7( the carrier of m,REAL) is complex-yielding V186() V187() set
K6(K7( the carrier of m,REAL)) is set
the U8 of m . (Z . f) is V11() real ext-real Element of REAL
k * ||.f.|| is V11() real ext-real Element of REAL
k * 1 is V11() real ext-real Element of REAL
modetrans (Z,Z0,m) is non empty Relation-like the carrier of Z0 -defined the carrier of m -valued Function-like total quasi_total V179(Z0,m) V180(Z0,m) Lipschitzian Element of K6(K7( the carrier of Z0, the carrier of m))
PreNorms (modetrans (Z,Z0,m)) is non empty V196() V197() V198() Element of K6(REAL)
{ ||.((modetrans (Z,Z0,m)) . b1).|| where b1 is Element of the carrier of Z0 : ||.b1.|| <= 1 } is set
I is ext-real set
i is Element of the carrier of Z0
(modetrans (Z,Z0,m)) . i is Element of the carrier of m
||.((modetrans (Z,Z0,m)) . i).|| is V11() real ext-real non negative Element of REAL
the U8 of m . ((modetrans (Z,Z0,m)) . i) is V11() real ext-real Element of REAL
||.i.|| is V11() real ext-real non negative Element of REAL
the U8 of Z0 . i is V11() real ext-real Element of REAL
f is non empty Relation-like the carrier of Z0 -defined the carrier of m -valued Function-like total quasi_total V179(Z0,m) V180(Z0,m) Lipschitzian Element of K6(K7( the carrier of Z0, the carrier of m))
f . i is Element of the carrier of m
||.(f . i).|| is V11() real ext-real non negative Element of REAL
the U8 of m . (f . i) is V11() real ext-real Element of REAL
upper_bound (PreNorms (modetrans (Z,Z0,m))) is V11() real ext-real Element of REAL
(upper_bound (PreNorms (modetrans (Z,Z0,m)))) - k is V11() real ext-real Element of REAL
(upper_bound (PreNorms (modetrans (Z,Z0,m)))) - ((upper_bound (PreNorms (modetrans (Z,Z0,m)))) - k) is V11() real ext-real Element of REAL
J is V11() real ext-real set
f is non empty Relation-like the carrier of Z0 -defined the carrier of m -valued Function-like total quasi_total V179(Z0,m) V180(Z0,m) Lipschitzian Element of K6(K7( the carrier of Z0, the carrier of m))
PreNorms f is non empty V196() V197() V198() Element of K6(REAL)
{ ||.(f . b1).|| where b1 is Element of the carrier of Z0 : ||.b1.|| <= 1 } is set
upper_bound (PreNorms f) is V11() real ext-real Element of REAL
Z0 is set
m is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() RealNormSpace-like NORMSTR
the carrier of m is non empty set
K7( the carrier of m,REAL) is complex-yielding V186() V187() set
K6(K7( the carrier of m,REAL)) is set
K7(NAT, the carrier of m) is set
K6(K7(NAT, the carrier of m)) is set
Z is Relation-like the carrier of m -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7( the carrier of m,REAL))
dom Z is Element of K6( the carrier of m)
K6( the carrier of m) is set
k is non empty Relation-like NAT -defined the carrier of m -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of m))
rng k is Element of K6( the carrier of m)
lim k is Element of the carrier of m
Z | Z0 is Relation-like the carrier of m -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7( the carrier of m,REAL))
dom (Z | Z0) is Element of K6( the carrier of m)
(dom Z) /\ Z0 is Element of K6( the carrier of m)
dom k is V196() V197() V198() V199() V200() V201() Element of K6(NAT)
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
k . f is Element of the carrier of m
(Z | Z0) /* k is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V186() V187() Element of K6(K7(NAT,REAL))
((Z | Z0) /* k) . f is V11() real ext-real Element of REAL
(Z | Z0) /. (k . f) is V11() real ext-real Element of REAL
Z /. (k . f) is V11() real ext-real Element of REAL
Z /* k is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V186() V187() Element of K6(K7(NAT,REAL))
(Z /* k) . f is V11() real ext-real Element of REAL
Z /. (lim k) is V11() real ext-real Element of REAL
(Z | Z0) /. (lim k) is V11() real ext-real Element of REAL
lim (Z /* k) is V11() real ext-real Element of REAL
k is non empty Relation-like NAT -defined the carrier of m -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of m))
rng k is Element of K6( the carrier of m)
lim k is Element of the carrier of m
Z /* k is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V186() V187() Element of K6(K7(NAT,REAL))
Z /. (lim k) is V11() real ext-real Element of REAL
lim (Z /* k) is V11() real ext-real Element of REAL
Z | Z0 is Relation-like the carrier of m -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7( the carrier of m,REAL))
dom (Z | Z0) is Element of K6( the carrier of m)
(dom Z) /\ Z0 is Element of K6( the carrier of m)
k is Element of the carrier of m
f is non empty Relation-like NAT -defined the carrier of m -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of m))
rng f is Element of K6( the carrier of m)
lim f is Element of the carrier of m
dom f is V196() V197() V198() V199() V200() V201() Element of K6(NAT)
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
f . g is Element of the carrier of m
(Z | Z0) /* f is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V186() V187() Element of K6(K7(NAT,REAL))
((Z | Z0) /* f) . g is V11() real ext-real Element of REAL
(Z | Z0) /. (f . g) is V11() real ext-real Element of REAL
Z /. (f . g) is V11() real ext-real Element of REAL
Z /* f is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-yielding V186() V187() Element of K6(K7(NAT,REAL))
(Z /* f) . g is V11() real ext-real Element of REAL
(Z | Z0) /. (lim f) is V11() real ext-real Element of REAL
Z /. (lim f) is V11() real ext-real Element of REAL
(Z | Z0) /. k is V11() real ext-real Element of REAL
lim ((Z | Z0) /* f) is V11() real ext-real Element of REAL
Z0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
REAL Z0 is non empty functional FinSequence-membered V263() V264() V265() FinSequenceSet of REAL
Z0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = Z0 } is set
K7((REAL Z0),REAL) is complex-yielding V186() V187() set
K6(K7((REAL Z0),REAL)) is set
m is Relation-like REAL Z0 -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7((REAL Z0),REAL))
<>* m is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
K7((REAL Z0),(REAL 1)) is set
K6(K7((REAL Z0),(REAL 1))) is set
m (#) ((proj (1,1)) ") is Relation-like Function-like set
dom (<>* m) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
K6((REAL Z0)) is set
dom m is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
rng m is V196() V197() V198() Element of K6(REAL)
Z is non empty Relation-like REAL -defined REAL 1 -valued Function-like total quasi_total V269() V270() V271() Element of K6(K7(REAL,(REAL 1)))
Z0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
REAL Z0 is non empty functional FinSequence-membered V263() V264() V265() FinSequenceSet of REAL
Z0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = Z0 } is set
K7((REAL Z0),REAL) is complex-yielding V186() V187() set
K6(K7((REAL Z0),REAL)) is set
m is set
Z is Relation-like REAL Z0 -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7((REAL Z0),REAL))
dom Z is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
K6((REAL Z0)) is set
<>* Z is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
K7((REAL Z0),(REAL 1)) is set
K6(K7((REAL Z0),(REAL 1))) is set
Z (#) ((proj (1,1)) ") is Relation-like Function-like set
(<>* Z) | m is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
dom ((<>* Z) | m) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
dom (<>* Z) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
Z0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
REAL Z0 is non empty functional FinSequence-membered V263() V264() V265() FinSequenceSet of REAL
Z0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = Z0 } is set
K7((REAL Z0),REAL) is complex-yielding V186() V187() set
K6(K7((REAL Z0),REAL)) is set
m is set
Z is Relation-like REAL Z0 -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7((REAL Z0),REAL))
Z | m is Relation-like REAL Z0 -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7((REAL Z0),REAL))
<>* (Z | m) is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
K7((REAL Z0),(REAL 1)) is set
K6(K7((REAL Z0),(REAL 1))) is set
(Z | m) (#) ((proj (1,1)) ") is Relation-like Function-like set
<>* Z is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
Z (#) ((proj (1,1)) ") is Relation-like Function-like set
(<>* Z) | m is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
rng (Z | m) is V196() V197() V198() Element of K6(REAL)
f is non empty Relation-like REAL -defined REAL 1 -valued Function-like total quasi_total V269() V270() V271() Element of K6(K7(REAL,(REAL 1)))
dom ((Z | m) (#) ((proj (1,1)) ")) is set
dom (Z | m) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
K6((REAL Z0)) is set
dom Z is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
(dom Z) /\ m is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
dom (<>* Z) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
(dom (<>* Z)) /\ m is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
f is set
dom ((<>* Z) | m) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
(<>* (Z | m)) . f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
(Z | m) . f is V11() real ext-real Element of REAL
((proj (1,1)) ") . ((Z | m) . f) is set
Z . f is V11() real ext-real Element of REAL
((proj (1,1)) ") . (Z . f) is set
(Z (#) ((proj (1,1)) ")) . f is set
((<>* Z) | m) . f is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
Z0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
REAL Z0 is non empty functional FinSequence-membered V263() V264() V265() FinSequenceSet of REAL
Z0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = Z0 } is set
K7((REAL Z0),REAL) is complex-yielding V186() V187() set
K6(K7((REAL Z0),REAL)) is set
m is Relation-like REAL Z0 -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7((REAL Z0),REAL))
dom m is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
K6((REAL Z0)) is set
<>* m is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
K7((REAL Z0),(REAL 1)) is set
K6(K7((REAL Z0),(REAL 1))) is set
m (#) ((proj (1,1)) ") is Relation-like Function-like set
Z is Relation-like NAT -defined REAL -valued Function-like V33() V40(Z0) FinSequence-like FinSubsequence-like complex-yielding V186() V187() Element of REAL Z0
(<>* m) . Z is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
m . Z is V11() real ext-real Element of REAL
<*(m . Z)*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,(m . Z)] is set
{1,(m . Z)} is non empty V196() V197() V198() set
{{1,(m . Z)},{1}} is non empty set
{[1,(m . Z)]} is non empty Function-like set
(<>* m) /. Z is Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() Element of REAL 1
m /. Z is V11() real ext-real Element of REAL
<*(m /. Z)*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,(m /. Z)] is set
{1,(m /. Z)} is non empty V196() V197() V198() set
{{1,(m /. Z)},{1}} is non empty set
{[1,(m /. Z)]} is non empty Function-like set
((proj (1,1)) ") . (m . Z) is set
dom (<>* m) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
Z0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
REAL Z0 is non empty functional FinSequence-membered V263() V264() V265() FinSequenceSet of REAL
Z0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = Z0 } is set
K7((REAL Z0),REAL) is complex-yielding V186() V187() set
K6(K7((REAL Z0),REAL)) is set
m is Relation-like REAL Z0 -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7((REAL Z0),REAL))
Z is Relation-like REAL Z0 -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7((REAL Z0),REAL))
m + Z is Relation-like REAL Z0 -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7((REAL Z0),REAL))
<>* (m + Z) is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
K7((REAL Z0),(REAL 1)) is set
K6(K7((REAL Z0),(REAL 1))) is set
(m + Z) (#) ((proj (1,1)) ") is Relation-like Function-like set
<>* m is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
m (#) ((proj (1,1)) ") is Relation-like Function-like set
<>* Z is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
Z (#) ((proj (1,1)) ") is Relation-like Function-like set
(<>* m) + (<>* Z) is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
K792((REAL Z0),(REAL Z0),(REAL 1),(REAL 1),(<>* m),(<>* Z)) is Relation-like (REAL Z0) /\ (REAL Z0) -defined K724((K719((REAL 1)) /\ K719((REAL 1)))) -valued Function-like V269() V270() V271() Element of K6(K7(((REAL Z0) /\ (REAL Z0)),K724((K719((REAL 1)) /\ K719((REAL 1))))))
(REAL Z0) /\ (REAL Z0) is set
K719((REAL 1)) is set
K719((REAL 1)) /\ K719((REAL 1)) is set
K724((K719((REAL 1)) /\ K719((REAL 1)))) is functional V263() V264() V265() set
K7(((REAL Z0) /\ (REAL Z0)),K724((K719((REAL 1)) /\ K719((REAL 1))))) is set
K6(K7(((REAL Z0) /\ (REAL Z0)),K724((K719((REAL 1)) /\ K719((REAL 1)))))) is set
m - Z is Relation-like REAL Z0 -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7((REAL Z0),REAL))
- Z is Relation-like REAL Z0 -defined Function-like complex-yielding V186() V187() set
K38(1) is non empty V11() real ext-real non positive negative set
K38(1) (#) Z is Relation-like REAL Z0 -defined Function-like complex-yielding V186() V187() set
m + (- Z) is Relation-like REAL Z0 -defined Function-like complex-yielding V186() V187() set
<>* (m - Z) is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
(m - Z) (#) ((proj (1,1)) ") is Relation-like Function-like set
(<>* m) - (<>* Z) is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
K798((REAL Z0),(REAL Z0),(REAL 1),(REAL 1),(<>* m),(<>* Z)) is Relation-like (REAL Z0) /\ (REAL Z0) -defined K724((K719((REAL 1)) /\ K719((REAL 1)))) -valued Function-like V269() V270() V271() Element of K6(K7(((REAL Z0) /\ (REAL Z0)),K724((K719((REAL 1)) /\ K719((REAL 1))))))
dom (<>* (m + Z)) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
K6((REAL Z0)) is set
dom (m + Z) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
dom (<>* (m - Z)) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
dom (m - Z) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
dom (<>* m) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
dom m is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
dom (<>* Z) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
dom Z is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
(dom (<>* m)) /\ (dom (<>* Z)) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
dom ((<>* m) + (<>* Z)) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
dom ((<>* m) - (<>* Z)) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
k is set
(dom m) /\ (dom Z) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
m . k is V11() real ext-real Element of REAL
<*(m . k)*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,(m . k)] is set
{1,(m . k)} is non empty V196() V197() V198() set
{{1,(m . k)},{1}} is non empty set
{[1,(m . k)]} is non empty Function-like set
(<>* m) . k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
Z . k is V11() real ext-real Element of REAL
<*(Z . k)*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,(Z . k)] is set
{1,(Z . k)} is non empty V196() V197() V198() set
{{1,(Z . k)},{1}} is non empty set
{[1,(Z . k)]} is non empty Function-like set
(<>* Z) . k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
(<>* (m + Z)) . k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
(m + Z) . k is V11() real ext-real Element of REAL
<*((m + Z) . k)*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,((m + Z) . k)] is set
{1,((m + Z) . k)} is non empty V196() V197() V198() set
{{1,((m + Z) . k)},{1}} is non empty set
{[1,((m + Z) . k)]} is non empty Function-like set
(m . k) + (Z . k) is V11() real ext-real Element of REAL
<*((m . k) + (Z . k))*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,((m . k) + (Z . k))] is set
{1,((m . k) + (Z . k))} is non empty V196() V197() V198() set
{{1,((m . k) + (Z . k))},{1}} is non empty set
{[1,((m . k) + (Z . k))]} is non empty Function-like set
((<>* m) . k) + ((<>* Z) . k) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
((<>* m) + (<>* Z)) . k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
k is set
m . k is V11() real ext-real Element of REAL
<*(m . k)*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,(m . k)] is set
{1,(m . k)} is non empty V196() V197() V198() set
{{1,(m . k)},{1}} is non empty set
{[1,(m . k)]} is non empty Function-like set
(<>* m) . k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
Z . k is V11() real ext-real Element of REAL
<*(Z . k)*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,(Z . k)] is set
{1,(Z . k)} is non empty V196() V197() V198() set
{{1,(Z . k)},{1}} is non empty set
{[1,(Z . k)]} is non empty Function-like set
(<>* Z) . k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
(<>* (m - Z)) . k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
(m - Z) . k is V11() real ext-real Element of REAL
<*((m - Z) . k)*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,((m - Z) . k)] is set
{1,((m - Z) . k)} is non empty V196() V197() V198() set
{{1,((m - Z) . k)},{1}} is non empty set
{[1,((m - Z) . k)]} is non empty Function-like set
(m . k) - (Z . k) is V11() real ext-real Element of REAL
<*((m . k) - (Z . k))*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,((m . k) - (Z . k))] is set
{1,((m . k) - (Z . k))} is non empty V196() V197() V198() set
{{1,((m . k) - (Z . k))},{1}} is non empty set
{[1,((m . k) - (Z . k))]} is non empty Function-like set
((<>* m) . k) - ((<>* Z) . k) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
- ((<>* Z) . k) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
K38(1) (#) ((<>* Z) . k) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
((<>* m) . k) + (- ((<>* Z) . k)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
((<>* m) - (<>* Z)) . k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
Z0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
REAL Z0 is non empty functional FinSequence-membered V263() V264() V265() FinSequenceSet of REAL
Z0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = Z0 } is set
K7((REAL Z0),REAL) is complex-yielding V186() V187() set
K6(K7((REAL Z0),REAL)) is set
m is Relation-like REAL Z0 -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7((REAL Z0),REAL))
<>* m is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
K7((REAL Z0),(REAL 1)) is set
K6(K7((REAL Z0),(REAL 1))) is set
m (#) ((proj (1,1)) ") is Relation-like Function-like set
Z is V11() real ext-real set
Z (#) m is Relation-like REAL Z0 -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7((REAL Z0),REAL))
<>* (Z (#) m) is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
(Z (#) m) (#) ((proj (1,1)) ") is Relation-like Function-like set
Z (#) (<>* m) is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
(<>* m) [#] Z is Relation-like REAL Z0 -defined K724(K719((REAL 1))) -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),K724(K719((REAL 1)))))
K719((REAL 1)) is set
K724(K719((REAL 1))) is functional V263() V264() V265() set
K7((REAL Z0),K724(K719((REAL 1)))) is set
K6(K7((REAL Z0),K724(K719((REAL 1))))) is set
dom (<>* (Z (#) m)) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
K6((REAL Z0)) is set
dom (Z (#) m) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
dom m is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
dom (<>* m) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
dom (Z (#) (<>* m)) is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
k is set
(<>* (Z (#) m)) . k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
(Z (#) m) . k is V11() real ext-real Element of REAL
<*((Z (#) m) . k)*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,((Z (#) m) . k)] is set
{1,((Z (#) m) . k)} is non empty V196() V197() V198() set
{{1,((Z (#) m) . k)},{1}} is non empty set
{[1,((Z (#) m) . k)]} is non empty Function-like set
m . k is V11() real ext-real Element of REAL
Z * (m . k) is V11() real ext-real Element of REAL
<*(Z * (m . k))*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,(Z * (m . k))] is set
{1,(Z * (m . k))} is non empty V196() V197() V198() set
{{1,(Z * (m . k))},{1}} is non empty set
{[1,(Z * (m . k))]} is non empty Function-like set
<*(m . k)*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,(m . k)] is set
{1,(m . k)} is non empty V196() V197() V198() set
{{1,(m . k)},{1}} is non empty set
{[1,(m . k)]} is non empty Function-like set
Z (#) <*(m . k)*> is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() Element of K6(K7(NAT,REAL))
(<>* m) . k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
Z (#) ((<>* m) . k) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
(Z (#) (<>* m)) . k is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
Z0 is V11() real ext-real Element of REAL
<*Z0*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,Z0] is set
{1,Z0} is non empty V196() V197() V198() set
{{1,Z0},{1}} is non empty set
{[1,Z0]} is non empty Function-like set
|.Z0.| is V11() real ext-real Element of REAL
m is Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() Element of REAL 1
|.m.| is V11() real ext-real non negative Element of REAL
sqr m is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
m (#) m is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
Sum (sqr m) is V11() real ext-real Element of REAL
sqrt (Sum (sqr m)) is V11() real ext-real Element of REAL
k is non empty Relation-like REAL -defined REAL 1 -valued Function-like total quasi_total V269() V270() V271() Element of K6(K7(REAL,(REAL 1)))
Z is non empty Relation-like REAL -defined REAL 1 -valued Function-like total quasi_total V269() V270() V271() Element of K6(K7(REAL,(REAL 1)))
Z . Z0 is Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() Element of REAL 1
k is Element of the carrier of (REAL-NS 1)
||.k.|| is V11() real ext-real non negative Element of REAL
the U8 of (REAL-NS 1) is non empty Relation-like the carrier of (REAL-NS 1) -defined REAL -valued Function-like total quasi_total complex-yielding V186() V187() Element of K6(K7( the carrier of (REAL-NS 1),REAL))
K7( the carrier of (REAL-NS 1),REAL) is complex-yielding V186() V187() set
K6(K7( the carrier of (REAL-NS 1),REAL)) is set
the U8 of (REAL-NS 1) . k is V11() real ext-real Element of REAL
Z0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
REAL Z0 is non empty functional FinSequence-membered V263() V264() V265() FinSequenceSet of REAL
Z0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = Z0 } is set
K7((REAL Z0),REAL) is complex-yielding V186() V187() set
K6(K7((REAL Z0),REAL)) is set
K7((REAL Z0),(REAL 1)) is set
K6(K7((REAL Z0),(REAL 1))) is set
m is Relation-like REAL Z0 -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7((REAL Z0),REAL))
<>* m is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
m (#) ((proj (1,1)) ") is Relation-like Function-like set
|.m.| is Relation-like REAL Z0 -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7((REAL Z0),REAL))
Z is Relation-like REAL Z0 -defined REAL 1 -valued Function-like V269() V270() V271() Element of K6(K7((REAL Z0),(REAL 1)))
|.Z.| is Relation-like REAL Z0 -defined REAL -valued Function-like complex-yielding V186() V187() Element of K6(K7((REAL Z0),REAL))
dom |.Z.| is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
K6((REAL Z0)) is set
dom Z is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
dom m is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
dom |.m.| is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
k is Relation-like NAT -defined REAL -valued Function-like V33() V40(Z0) FinSequence-like FinSubsequence-like complex-yielding V186() V187() Element of REAL Z0
Z /. k is Relation-like NAT -defined Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() Element of REAL 1
m /. k is V11() real ext-real Element of REAL
<*(m /. k)*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,(m /. k)] is set
{1,(m /. k)} is non empty V196() V197() V198() set
{{1,(m /. k)},{1}} is non empty set
{[1,(m /. k)]} is non empty Function-like set
|.Z.| . k is V11() real ext-real Element of REAL
|.Z.| /. k is V11() real ext-real Element of REAL
|.(Z /. k).| is V11() real ext-real non negative Element of REAL
sqr (Z /. k) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
(Z /. k) (#) (Z /. k) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
Sum (sqr (Z /. k)) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (Z /. k))) is V11() real ext-real Element of REAL
|.(m /. k).| is V11() real ext-real Element of REAL
m . k is V11() real ext-real Element of REAL
|.(m . k).| is V11() real ext-real Element of REAL
|.m.| . k is V11() real ext-real Element of REAL
Z0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
REAL Z0 is non empty functional FinSequence-membered V263() V264() V265() FinSequenceSet of REAL
Z0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = Z0 } is set
K6((REAL Z0)) is set
REAL-NS Z0 is non empty V50() V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() strict RealNormSpace-like V182() NORMSTR
the carrier of (REAL-NS Z0) is non empty V2() set
K6( the carrier of (REAL-NS Z0)) is set
m is functional FinSequence-membered V263() V264() V265() Element of K6((REAL Z0))
Z is Element of K6( the carrier of (REAL-NS Z0))
k is Element of K6( the carrier of (REAL-NS Z0))
Z0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
REAL m is non empty functional FinSequence-membered V263() V264() V265() FinSequenceSet of REAL
m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = m } is set
0* m is Relation-like NAT -defined REAL -valued Function-like V33() V40(m) FinSequence-like FinSubsequence-like complex-yielding V186() V187() Element of REAL m
m |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V33() V40(m) FinSequence-like FinSubsequence-like complex-yielding V186() V187() Element of m -tuples_on REAL
Seg m is V33() V40(m) V196() V197() V198() V199() V200() V201() Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
K256((Seg m),0) is Relation-like Seg m -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() V188() Element of K6(K7((Seg m),{0}))
{0} is non empty V196() V197() V198() V199() V200() V201() set
K7((Seg m),{0}) is INT -valued RAT -valued complex-yielding V186() V187() V188() set
K6(K7((Seg m),{0})) is set
reproj (Z0,(0* m)) is non empty Relation-like REAL -defined REAL m -valued Function-like total quasi_total V269() V270() V271() Element of K6(K7(REAL,(REAL m)))
K7(REAL,(REAL m)) is set
K6(K7(REAL,(REAL m))) is set
Z is V11() real ext-real Element of REAL
(reproj (Z0,(0* m))) . Z is Relation-like NAT -defined Function-like V33() V40(m) FinSequence-like FinSubsequence-like complex-yielding V186() V187() Element of REAL m
|.((reproj (Z0,(0* m))) . Z).| is V11() real ext-real non negative Element of REAL
sqr ((reproj (Z0,(0* m))) . Z) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
((reproj (Z0,(0* m))) . Z) (#) ((reproj (Z0,(0* m))) . Z) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
Sum (sqr ((reproj (Z0,(0* m))) . Z)) is V11() real ext-real Element of REAL
sqrt (Sum (sqr ((reproj (Z0,(0* m))) . Z))) is V11() real ext-real Element of REAL
|.Z.| is V11() real ext-real Element of REAL
Replace ((0* m),Z0,Z) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
Z0 -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
(0* m) | (Z0 -' 1) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
Seg (Z0 -' 1) is V33() V40(Z0 -' 1) V196() V197() V198() V199() V200() V201() Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT : ( 1 <= b1 & b1 <= Z0 -' 1 ) } is set
(0* m) | (Seg (Z0 -' 1)) is Relation-like NAT -defined Function-like FinSubsequence-like complex-yielding V186() V187() set
<*Z*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() V40(1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
[1,Z] is set
{1,Z} is non empty V196() V197() V198() set
{{1,Z},{1}} is non empty set
{[1,Z]} is non empty Function-like set
((0* m) | (Z0 -' 1)) ^ <*Z*> is non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
(0* m) /^ Z0 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
(((0* m) | (Z0 -' 1)) ^ <*Z*>) ^ ((0* m) /^ Z0) is non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
f is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() Element of REAL *
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
sqr ((0* m) | (Z0 -' 1)) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
((0* m) | (Z0 -' 1)) (#) ((0* m) | (Z0 -' 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
Sum (sqr ((0* m) | (Z0 -' 1))) is V11() real ext-real Element of REAL
sqrt (Sum (sqr ((0* m) | (Z0 -' 1)))) is V11() real ext-real Element of REAL
0* (Z0 -' 1) is Relation-like NAT -defined REAL -valued Function-like V33() V40(Z0 -' 1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() Element of REAL (Z0 -' 1)
REAL (Z0 -' 1) is non empty functional FinSequence-membered V263() V264() V265() FinSequenceSet of REAL
(Z0 -' 1) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = Z0 -' 1 } is set
(Z0 -' 1) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V33() V40(Z0 -' 1) FinSequence-like FinSubsequence-like complex-yielding V186() V187() Element of (Z0 -' 1) -tuples_on REAL
K256((Seg (Z0 -' 1)),0) is Relation-like Seg (Z0 -' 1) -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() V188() Element of K6(K7((Seg (Z0 -' 1)),{0}))
K7((Seg (Z0 -' 1)),{0}) is INT -valued RAT -valued complex-yielding V186() V187() V188() set
K6(K7((Seg (Z0 -' 1)),{0})) is set
|.(0* (Z0 -' 1)).| is V11() real ext-real non negative Element of REAL
sqr (0* (Z0 -' 1)) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
(0* (Z0 -' 1)) (#) (0* (Z0 -' 1)) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
Sum (sqr (0* (Z0 -' 1))) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (0* (Z0 -' 1)))) is V11() real ext-real Element of REAL
sqr ((0* m) /^ Z0) is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() FinSequence of REAL
((0* m) /^ Z0) (#) ((0* m) /^ Z0) is Relation-like NAT -defined Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V186() V187() set
Sum (sqr ((0* m) /^ Z0)) is V11() real ext-real Element of REAL
sqrt (Sum (sqr ((0* m) /^ Z0))) is V11() real ext-real Element of REAL
m -' Z0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT
0* (m -' Z0) is Relation-like NAT -defined REAL -valued Function-like V33() V40(m -' Z0) FinSequence-like FinSubsequence-like complex-yielding V186() V187() Element of REAL (m -' Z0)
REAL (m -' Z0) is non empty functional FinSequence-membered V263() V264() V265() FinSequenceSet of REAL
(m -' Z0) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = m -' Z0 } is set
(m -' Z0) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like V33() V40(m -' Z0) FinSequence-like FinSubsequence-like complex-yielding V186() V187() Element of (m -' Z0) -tuples_on REAL
Seg (m -' Z0) is V33() V40(m -' Z0) V196() V197() V198() V199() V200() V201() Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V160() V195() V196() V197() V198() V199() V200() V201() Element of NAT : ( 1