REAL is non empty non finite complex-membered ext-real-membered real-membered V205() non bounded_below non bounded_above V263() set
NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V205() bounded_below 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 non finite complex-membered V205() set
omega is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V205() bounded_below set
K6(omega) is set
K6(NAT) is set
K7(NAT,REAL) is complex-valued ext-real-valued real-valued 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-valued ext-real-valued real-valued set
K6(K7(K7(K200(),K200()),REAL)) is set
K203() is Element of K6( the carrier of K196())
K7(K203(),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K203(),REAL)) is set
1 is non empty ordinal natural V11() real ext-real positive non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
INT is non empty non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V205() set
K7(1,1) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
RAT is non empty non finite complex-membered ext-real-membered real-membered rational-membered V205() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is complex-valued ext-real-valued real-valued set
K7(K7(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty ordinal natural V11() real ext-real positive non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
K7(2,2) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K7(K7(2,2),REAL) is complex-valued ext-real-valued real-valued 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 V148() V214() V215() L19()
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite 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 V185() 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 V185() 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 V214() RLSStruct
LinearOperators ((REAL-NS 1),(REAL-NS 1)) is non empty functional Element of K6( the carrier of K318( the carrier of (REAL-NS 1),(REAL-NS 1)))
K318( 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 V214() 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))
0. (REAL-NS 1) is V52( REAL-NS 1) Element of the carrier of (REAL-NS 1)
K214( 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 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 K318( the carrier of (REAL-NS 1),(REAL-NS 1)) is non empty set
K6( the carrier of K318( the carrier of (REAL-NS 1),(REAL-NS 1))) is set
K199(K318( 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(K318( 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(K318( 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(K318( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),K197(K318( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),K198(K318( 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-valued ext-real-valued real-valued Element of K6(K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),REAL))
K7((BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1))),REAL) is complex-valued ext-real-valued real-valued 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-valued set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is RAT -valued complex-valued ext-real-valued real-valued set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is RAT -valued complex-valued ext-real-valued real-valued set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K7(K7(NAT,NAT),NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(NAT,NAT),NAT)) is set
K541() is non empty V73() L8()
the carrier of K541() is non empty set
K546() is non empty V73() V164() V165() V166() V168() V224() V225() V226() V227() V228() V229() L8()
K547() is non empty V73() V166() V168() V227() V228() V229() M17(K546())
K548() is non empty V73() V164() V166() V168() V227() V228() V229() V230() M20(K546(),K547())
K550() is non empty V73() V164() V166() V168() L8()
K551() is non empty V73() V164() V166() V168() V230() M17(K550())
ExtREAL is non empty ext-real-membered V263() set
{} is empty Function-like functional FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V205() bounded_below V263() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered set
the empty Function-like functional FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V205() bounded_below V263() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered set is empty Function-like functional FinSequence-membered complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V205() bounded_below V263() 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
K310() is V94() L11()
the carrier of K310() is set
the carrier of K310() * is non empty functional FinSequence-membered FinSequenceSet of the carrier of K310()
K7(COMPLEX,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(COMPLEX,REAL)) is set
3 is non empty ordinal natural V11() real ext-real positive non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT
0 is empty ordinal natural V11() real ext-real non positive non negative Function-like functional FinSequence-membered V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V205() bounded_below V263() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered Element of NAT
sqrreal is non empty Relation-like REAL -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
sqrt 1 is V11() real ext-real Element of REAL
proj (1,1) is non empty Relation-like REAL 1 -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL 1),REAL))
K7((REAL 1),REAL) is complex-valued ext-real-valued real-valued 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
proj1 ((proj (1,1)) ") is set
proj2 ((proj (1,1)) ") is set
<*1*> is non empty V2() Relation-like NAT -defined NAT -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing FinSequence of NAT
[1,1] is V27() set
{1,1} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below set
{1} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below set
{{1,1},{1}} is non empty set
{[1,1]} is non empty Function-like set
m is ordinal natural V11() real ext-real non negative set
TOP-REAL m is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V148() V214() V215() L19()
the carrier of (TOP-REAL m) is non empty set
f is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
X is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
y0 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
f + X is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
f + X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
i + y0 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
f + X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
X is ordinal natural V11() real ext-real non negative set
TOP-REAL X is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V148() V214() V215() L19()
the carrier of (TOP-REAL X) is non empty set
m is V11() real ext-real set
f is V11() real ext-real set
i is Relation-like NAT -defined Function-like finite X -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL X)
y0 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
m * i is Relation-like NAT -defined Function-like finite X -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL X)
m * i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
f * y0 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
m is ordinal natural V11() real ext-real non negative set
TOP-REAL m is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V148() V214() V215() L19()
the carrier of (TOP-REAL m) is non empty set
f is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
- f is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
- f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K38(1) is non empty V11() real ext-real non positive negative set
K38(1) * f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
- X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K38(1) * X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
- f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
m is ordinal natural V11() real ext-real non negative set
TOP-REAL m is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V148() V214() V215() L19()
the carrier of (TOP-REAL m) is non empty set
f is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
X is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
y0 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
f - X is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
f - X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
- X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K38(1) * X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
f + (- X) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
i - y0 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
- y0 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K38(1) * y0 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
i + (- y0) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
f - X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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
f is Element of the carrier of m
X is Neighbourhood of f
i is Neighbourhood of f
X /\ i is Element of K6( the carrier of m)
K6( the carrier of m) is set
y0 is Neighbourhood of f
r is V11() real ext-real Element of REAL
{ b1 where b1 is Element of the carrier of m : not r <= ||.(b1 - f).|| } is set
m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
f is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
f -' m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
m + (f -' m) is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
m + f is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(m + f) -' m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
f - m is V11() real ext-real V163() V198() Element of INT
(m + f) - m is V11() real ext-real V163() V198() Element of INT
m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0* m is Relation-like NAT -defined REAL -valued Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL m
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = m } is set
m |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of m -tuples_on REAL
Seg m is finite m -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
K213((Seg m),0) is Relation-like Seg m -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg m),{0}))
{0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below set
K7((Seg m),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg m),{0})) is set
f is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0* f is Relation-like NAT -defined REAL -valued Function-like finite f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL f
REAL f is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is set
f |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL
Seg f is finite f -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
K213((Seg f),0) is Relation-like Seg f -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg f),{0}))
K7((Seg f),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg f),{0})) is set
(0* f) | m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(0* f) | (Seg m) is Relation-like NAT -defined Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len (0* m) is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
f -' m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0* (f -' m) is Relation-like NAT -defined REAL -valued Function-like finite f -' m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (f -' m)
REAL (f -' m) is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
(f -' 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 finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f -' m } is set
(f -' m) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite f -' m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f -' m) -tuples_on REAL
Seg (f -' m) is finite f -' m -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= f -' m ) } is set
K213((Seg (f -' m)),0) is Relation-like Seg (f -' m) -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg (f -' m)),{0}))
K7((Seg (f -' m)),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg (f -' m)),{0})) is set
(0* m) ^ (0* (f -' m)) is Relation-like NAT -defined REAL -valued Function-like finite K335(m,(f -' m)) -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K335(m,(f -' m)) is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
((0* m) ^ (0* (f -' m))) | (len (0* m)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Seg (len (0* m)) is finite len (0* m) -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= len (0* m) ) } is set
((0* m) ^ (0* (f -' m))) | (Seg (len (0* m))) is Relation-like NAT -defined Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
m + (f -' m) is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
m + f is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(m + f) -' m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(m + f) - m is V11() real ext-real V163() V198() Element of INT
m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
m -' 1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0* (m -' 1) is Relation-like NAT -defined REAL -valued Function-like finite m -' 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (m -' 1)
REAL (m -' 1) is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
(m -' 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 finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = m -' 1 } is set
(m -' 1) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite m -' 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (m -' 1) -tuples_on REAL
Seg (m -' 1) is finite m -' 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= m -' 1 ) } is set
K213((Seg (m -' 1)),0) is Relation-like Seg (m -' 1) -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg (m -' 1)),{0}))
{0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below set
K7((Seg (m -' 1)),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg (m -' 1)),{0})) is set
f is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0* f is Relation-like NAT -defined REAL -valued Function-like finite f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL f
REAL f is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is set
f |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL
Seg f is finite f -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
K213((Seg f),0) is Relation-like Seg f -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg f),{0}))
K7((Seg f),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg f),{0})) is set
(0* f) | (m -' 1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(0* f) | (Seg (m -' 1)) is Relation-like NAT -defined Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
m - 1 is V11() real ext-real V163() V198() Element of INT
f - 1 is V11() real ext-real V163() V198() Element of INT
m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
f is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0* f is Relation-like NAT -defined REAL -valued Function-like finite f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL f
REAL f is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is set
f |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL
Seg f is finite f -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
K213((Seg f),0) is Relation-like Seg f -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg f),{0}))
{0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below set
K7((Seg f),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg f),{0})) is set
(0* f) /^ m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
f -' m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0* (f -' m) is Relation-like NAT -defined REAL -valued Function-like finite f -' m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (f -' m)
REAL (f -' m) is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
(f -' 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 finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f -' m } is set
(f -' m) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite f -' m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f -' m) -tuples_on REAL
Seg (f -' m) is finite f -' m -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= f -' m ) } is set
K213((Seg (f -' m)),0) is Relation-like Seg (f -' m) -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg (f -' m)),{0}))
K7((Seg (f -' m)),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg (f -' m)),{0})) is set
len ((0* f) /^ m) is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
len (0* f) is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(len (0* f)) -' m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
len (0* (f -' m)) is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
X is ordinal natural V11() real ext-real non negative set
((0* f) /^ m) . X is V11() real ext-real Element of REAL
(0* (f -' m)) . X is V11() real ext-real Element of REAL
dom ((0* f) /^ m) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of K6(NAT)
X + m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(0* f) . (X + m) is V11() real ext-real Element of REAL
m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
f is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0* f is Relation-like NAT -defined REAL -valued Function-like finite f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL f
REAL f is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is set
f |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL
Seg f is finite f -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
K213((Seg f),0) is Relation-like Seg f -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg f),{0}))
{0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below set
K7((Seg f),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg f),{0})) is set
(0* f) /^ m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
f -' m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0* (f -' m) is Relation-like NAT -defined REAL -valued Function-like finite f -' m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (f -' m)
REAL (f -' m) is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
(f -' 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 finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f -' m } is set
(f -' m) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite f -' m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f -' m) -tuples_on REAL
Seg (f -' m) is finite f -' m -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= f -' m ) } is set
K213((Seg (f -' m)),0) is Relation-like Seg (f -' m) -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg (f -' m)),{0}))
K7((Seg (f -' m)),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg (f -' m)),{0})) is set
len (0* f) is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
f - m is V11() real ext-real V163() V198() Element of INT
m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0* m is Relation-like NAT -defined REAL -valued Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL m
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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = m } is set
m |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of m -tuples_on REAL
Seg m is finite m -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
K213((Seg m),0) is Relation-like Seg m -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg m),{0}))
{0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below set
K7((Seg m),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg m),{0})) is set
f is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
(0* m) /^ f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
m -' f is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0* (m -' f) is Relation-like NAT -defined REAL -valued Function-like finite m -' f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (m -' f)
REAL (m -' f) is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
(m -' f) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = m -' f } is set
(m -' f) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite m -' f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (m -' f) -tuples_on REAL
Seg (m -' f) is finite m -' f -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= m -' f ) } is set
K213((Seg (m -' f)),0) is Relation-like Seg (m -' f) -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg (m -' f)),{0}))
K7((Seg (m -' f)),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg (m -' f)),{0})) is set
m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
f is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
m -' 1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0* f is Relation-like NAT -defined REAL -valued Function-like finite f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL f
REAL f is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is set
f |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL
Seg f is finite f -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
K213((Seg f),0) is Relation-like Seg f -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg f),{0}))
{0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below set
K7((Seg f),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg f),{0})) is set
(0* f) | (m -' 1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Seg (m -' 1) is finite m -' 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= m -' 1 ) } is set
(0* f) | (Seg (m -' 1)) is Relation-like NAT -defined Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
0* (m -' 1) is Relation-like NAT -defined REAL -valued Function-like finite m -' 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (m -' 1)
REAL (m -' 1) is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
(m -' 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 finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = m -' 1 } is set
(m -' 1) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite m -' 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (m -' 1) -tuples_on REAL
K213((Seg (m -' 1)),0) is Relation-like Seg (m -' 1) -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg (m -' 1)),{0}))
K7((Seg (m -' 1)),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg (m -' 1)),{0})) is set
X is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
i is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0* i is Relation-like NAT -defined REAL -valued Function-like finite i -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL i
REAL i is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
i -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = i } is set
i |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite i -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of i -tuples_on REAL
Seg i is finite i -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= i ) } is set
K213((Seg i),0) is Relation-like Seg i -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg i),{0}))
K7((Seg i),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg i),{0})) is set
(0* i) /^ X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
i -' X is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0* (i -' X) is Relation-like NAT -defined REAL -valued Function-like finite i -' X -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (i -' X)
REAL (i -' X) is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
(i -' X) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = i -' X } is set
(i -' X) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite i -' X -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (i -' X) -tuples_on REAL
Seg (i -' X) is finite i -' X -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= i -' X ) } is set
K213((Seg (i -' X)),0) is Relation-like Seg (i -' X) -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg (i -' X)),{0}))
K7((Seg (i -' X)),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg (i -' X)),{0})) is set
m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
f is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
REAL-NS f is non empty V71() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() V107() strict RealNormSpace-like V185() NORMSTR
the carrier of (REAL-NS f) is non empty set
0. (REAL-NS f) is V52( REAL-NS f) Element of the carrier of (REAL-NS f)
reproj (m,(0. (REAL-NS f))) is non empty Relation-like the carrier of (REAL-NS 1) -defined the carrier of (REAL-NS f) -valued Function-like total quasi_total Element of K6(K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS f)))
K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS f)) is set
K6(K7( the carrier of (REAL-NS 1), the carrier of (REAL-NS f))) is set
X is Element of the carrier of (REAL-NS 1)
(reproj (m,(0. (REAL-NS f)))) . X is Element of the carrier of (REAL-NS f)
||.((reproj (m,(0. (REAL-NS f)))) . X).|| is V11() real ext-real Element of REAL
the U8 of (REAL-NS f) is non empty Relation-like the carrier of (REAL-NS f) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7( the carrier of (REAL-NS f),REAL))
K7( the carrier of (REAL-NS f),REAL) is complex-valued ext-real-valued real-valued set
K6(K7( the carrier of (REAL-NS f),REAL)) is set
the U8 of (REAL-NS f) . ((reproj (m,(0. (REAL-NS f)))) . X) is V11() real ext-real Element of REAL
||.X.|| is V11() real ext-real 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-valued ext-real-valued real-valued Element of K6(K7( the carrier of (REAL-NS 1),REAL))
K7( the carrier of (REAL-NS 1),REAL) is complex-valued ext-real-valued real-valued set
K6(K7( the carrier of (REAL-NS 1),REAL)) is set
the U8 of (REAL-NS 1) . X is V11() real ext-real Element of REAL
REAL f is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
f -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f } is set
i is V11() real ext-real Element of REAL
<*i*> is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing FinSequence of REAL
[1,i] is V27() set
{1,i} is non empty complex-membered ext-real-membered real-membered set
{{1,i},{1}} is non empty set
{[1,i]} is non empty Function-like set
y0 is Relation-like NAT -defined REAL -valued Function-like finite f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL f
reproj (m,y0) is non empty Relation-like REAL -defined REAL f -valued Function-like total quasi_total complex-functions-valued ext-real-functions-valued real-functions-valued Element of K6(K7(REAL,(REAL f)))
K7(REAL,(REAL f)) is set
K6(K7(REAL,(REAL f))) is set
(reproj (m,y0)) . i is Relation-like NAT -defined Function-like finite f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL f
Replace (y0,m,i) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len y0 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
m -' 1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
y0 | (m -' 1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Seg (m -' 1) is finite m -' 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= m -' 1 ) } is set
y0 | (Seg (m -' 1)) is Relation-like NAT -defined Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(y0 | (m -' 1)) ^ <*i*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
y0 /^ m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
((y0 | (m -' 1)) ^ <*i*>) ^ (y0 /^ m) is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
|.(((y0 | (m -' 1)) ^ <*i*>) ^ (y0 /^ m)).| is V11() real ext-real non negative Element of REAL
sqr (((y0 | (m -' 1)) ^ <*i*>) ^ (y0 /^ m)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
mlt ((((y0 | (m -' 1)) ^ <*i*>) ^ (y0 /^ m)),(((y0 | (m -' 1)) ^ <*i*>) ^ (y0 /^ m))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (sqr (((y0 | (m -' 1)) ^ <*i*>) ^ (y0 /^ m))) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (((y0 | (m -' 1)) ^ <*i*>) ^ (y0 /^ m)))) is V11() real ext-real Element of REAL
0* f is Relation-like NAT -defined REAL -valued Function-like finite f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL f
f |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite f -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of f -tuples_on REAL
Seg f is finite f -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= f ) } is set
K213((Seg f),0) is Relation-like Seg f -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg f),{0}))
{0} is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below set
K7((Seg f),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg f),{0})) is set
(0* f) | (m -' 1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(0* f) | (Seg (m -' 1)) is Relation-like NAT -defined Function-like FinSubsequence-like complex-valued ext-real-valued real-valued set
sqr (y0 | (m -' 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
mlt ((y0 | (m -' 1)),(y0 | (m -' 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (sqr (y0 | (m -' 1))) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (y0 | (m -' 1)))) is V11() real ext-real Element of REAL
0* (m -' 1) is Relation-like NAT -defined REAL -valued Function-like finite m -' 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (m -' 1)
REAL (m -' 1) is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
(m -' 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 finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = m -' 1 } is set
(m -' 1) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite m -' 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (m -' 1) -tuples_on REAL
K213((Seg (m -' 1)),0) is Relation-like Seg (m -' 1) -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg (m -' 1)),{0}))
K7((Seg (m -' 1)),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg (m -' 1)),{0})) is set
|.(0* (m -' 1)).| is V11() real ext-real non negative Element of REAL
sqr (0* (m -' 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
mlt ((0* (m -' 1)),(0* (m -' 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (sqr (0* (m -' 1))) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (0* (m -' 1)))) is V11() real ext-real Element of REAL
(0* f) /^ m is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
sqr (y0 /^ m) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
mlt ((y0 /^ m),(y0 /^ m)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (sqr (y0 /^ m)) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (y0 /^ m))) is V11() real ext-real Element of REAL
f -' m is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT
0* (f -' m) is Relation-like NAT -defined REAL -valued Function-like finite f -' m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (f -' m)
REAL (f -' m) is non empty functional FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
(f -' 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 finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = f -' m } is set
(f -' m) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite f -' m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (f -' m) -tuples_on REAL
Seg (f -' m) is finite f -' m -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of K6(NAT)
{ b1 where b1 is ordinal natural V11() real ext-real non negative V163() V198() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT : ( 1 <= b1 & b1 <= f -' m ) } is set
K213((Seg (f -' m)),0) is Relation-like Seg (f -' m) -defined INT -valued RAT -valued {0} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K6(K7((Seg (f -' m)),{0}))
K7((Seg (f -' m)),{0}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7((Seg (f -' m)),{0})) is set
|.(0* (f -' m)).| is V11() real ext-real non negative Element of REAL
sqr (0* (f -' m)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
mlt ((0* (f -' m)),(0* (f -' m))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum (sqr (0* (f -' m))) is V11() real ext-real Element of REAL
sqrt (Sum (sqr (0* (f -' m)))) is V11() real ext-real Element of REAL
sqr ((y0 | (m -' 1)) ^ <*i*>) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
mlt (((y0 | (m -' 1)) ^ <*i*>),((y0 | (m -' 1)) ^ <*i*>)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(sqr ((y0 | (m -' 1)) ^ <*i*>)) ^ (sqr (y0 /^ m)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
sqr <*i*> is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
mlt (<*i*>,<*i*>) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(sqr (y0 | (m -' 1))) ^ (sqr <*i*>) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
((sqr (y0 | (m -' 1))) ^ (sqr <*i*>)) ^ (sqr (y0 /^ m)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
i ^2 is V11() real ext-real Element of REAL
K37(i,i) is V11() real ext-real set
<*(i ^2)*> is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing FinSequence of REAL
[1,(i ^2)] is V27() set
{1,(i ^2)} is non empty complex-membered ext-real-membered real-membered set
{{1,(i ^2)},{1}} is non empty set
{[1,(i ^2)]} is non empty Function-like set
(sqr (y0 | (m -' 1))) ^ <*(i ^2)*> is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
((sqr (y0 | (m -' 1))) ^ <*(i ^2)*>) ^ (sqr (y0 /^ m)) is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Sum ((sqr (y0 | (m -' 1))) ^ <*(i ^2)*>) is V11() real ext-real Element of REAL
(Sum ((sqr (y0 | (m -' 1))) ^ <*(i ^2)*>)) + (Sum (sqr (y0 /^ m))) is V11() real ext-real Element of REAL
(Sum (sqr (y0 | (m -' 1)))) + (i ^2) is V11() real ext-real Element of REAL
((Sum (sqr (y0 | (m -' 1)))) + (i ^2)) + (Sum (sqr (y0 /^ m))) is V11() real ext-real Element of REAL
|.i.| is V11() real ext-real Element of REAL
(proj (1,1)) . <*i*> is V11() real ext-real Element of REAL
m is