:: PDIFF_7 semantic presentation

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

{ b

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

{ b

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

{ b

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)

{ b

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

{ b

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)

{ b

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

{ b

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

{ b

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)

{ b

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

{ b

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

{ b

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

{ b

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)

{ b

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

{ b

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)

{ b

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

{ b

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

{ b

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

{ b

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)

{ b

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

{ b

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

{ b

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

{ b

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)

{ b

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

{ b

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

{ b

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

{ b

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)

{ b

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)

{ b

(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

{ b

(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

{ b

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)

{ b

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

{ b

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

{ b

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

{ b

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)

{ b

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)

{ b

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

{ b

(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

{ b

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

{ b

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