REAL is non empty V49() V160() V161() V162() V166() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V160() V161() V162() V163() V164() V165() V166() Element of K6(REAL)
K6(REAL) is set
REAL * is functional FinSequence-membered FinSequenceSet of REAL
K7(NAT,(REAL *)) is set
K6(K7(NAT,(REAL *))) is set
COMPLEX is non empty V49() V160() V166() set
K7(REAL,REAL) is complex-valued ext-real-valued real-valued set
K6(K7(REAL,REAL)) is set
omega is non empty epsilon-transitive epsilon-connected ordinal V160() V161() V162() V163() V164() V165() V166() 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
K224() is non empty set
K7(K224(),K224()) is set
K7(K7(K224(),K224()),K224()) is set
K6(K7(K7(K224(),K224()),K224())) is set
K7(REAL,K224()) is set
K7(K7(REAL,K224()),K224()) is set
K6(K7(K7(REAL,K224()),K224())) is set
K230() is RLSStruct
the carrier of K230() is set
K6( the carrier of K230()) is set
K234() is Element of K6( the carrier of K230())
K7(K234(),K234()) is set
K7(K7(K234(),K234()),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(K234(),K234()),REAL)) is set
ExtREAL is non empty V161() set
RAT is non empty V49() V160() V161() V162() V163() V166() set
INT is non empty V49() V160() V161() V162() V163() V164() V166() 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(K7(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K6(K7(K7(REAL,REAL),REAL)) 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
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
K7(1,1) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued 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
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() 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
TOP-REAL 2 is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V202() L20()
the carrier of (TOP-REAL 2) is non empty set
REAL 1 is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7((REAL 1),(REAL 1)) is set
K6(K7((REAL 1),(REAL 1))) is set
REAL-NS 1 is non empty non trivial V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() strict RealNormSpace-like V156() NORMSTR
the carrier of (REAL-NS 1) is non empty non trivial set
R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)) is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() RealNormSpace-like V156() 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 V87() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
LinearOperators ((REAL-NS 1),(REAL-NS 1)) is non empty functional Element of K6( the carrier of K284( the carrier of (REAL-NS 1),(REAL-NS 1)))
K284( the carrier of (REAL-NS 1),(REAL-NS 1)) is non empty V87() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital 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 V68( REAL-NS 1) Element of the carrier of (REAL-NS 1)
the ZeroF of (REAL-NS 1) is Element of the carrier of (REAL-NS 1)
the carrier of (REAL-NS 1) --> (0. (REAL-NS 1)) is non empty Relation-like the carrier of (REAL-NS 1) -defined the carrier of (REAL-NS 1) -valued Function-like total 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 K284( the carrier of (REAL-NS 1),(REAL-NS 1)) is non empty set
K6( the carrier of K284( the carrier of (REAL-NS 1),(REAL-NS 1))) is set
K233(K284( 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))
K231(K284( 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
K232(K284( 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))),K233(K284( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),K231(K284( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))),K232(K284( the carrier of (REAL-NS 1),(REAL-NS 1)),(LinearOperators ((REAL-NS 1),(REAL-NS 1)))) #) is V87() 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
K233((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))
K231((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
K232((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))),K233((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),K231((R_VectorSpace_of_LinearOperators ((REAL-NS 1),(REAL-NS 1))),(BoundedLinearOperators ((REAL-NS 1),(REAL-NS 1)))),K232((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
TOP-REAL 1 is non empty V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V202() L20()
the carrier of (TOP-REAL 1) is non empty set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V160() V161() V162() V163() V164() V165() V166() V233() V234() V235() V236() V237() V238() set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V132() V159() V160() V161() V162() V163() V164() V165() V166() V233() V234() V235() V236() V237() V238() Element of NAT
- 1 is V11() real ext-real non positive Element of REAL
|.0.| is V11() real ext-real V159() Element of REAL
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))
proj (1,1) is non empty Relation-like REAL 1 -defined REAL 1 -defined REAL -valued Function-like one-to-one total total quasi_total quasi_total onto bijective 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 one-to-one set
K7(REAL,(REAL 1)) is set
K6(K7(REAL,(REAL 1))) is set
dom ((proj (1,1)) ") is set
rng ((proj (1,1)) ") is set
- 1 is V11() real ext-real non positive Element of REAL
NAT --> 0 is non empty T-Sequence-like Relation-like NAT -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K6(K7(NAT,NAT))
K6(K7(NAT,NAT)) is set
[#] REAL is V160() V161() V162() closed open Element of K6(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL n is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is set
K6(K7(REAL,(REAL n))) is set
m is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
x0 is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
m - x0 is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
K714(REAL,REAL,(REAL n),(REAL n),m,x0) is Relation-like REAL /\ REAL -defined K640((K635((REAL n)) /\ K635((REAL n)))) -valued Function-like V239() V240() V241() Element of K6(K7((REAL /\ REAL),K640((K635((REAL n)) /\ K635((REAL n))))))
REAL /\ REAL is V160() V161() V162() set
K635((REAL n)) is set
K635((REAL n)) /\ K635((REAL n)) is set
K640((K635((REAL n)) /\ K635((REAL n)))) is functional V233() V234() V235() set
K7((REAL /\ REAL),K640((K635((REAL n)) /\ K635((REAL n))))) is set
K6(K7((REAL /\ REAL),K640((K635((REAL n)) /\ K635((REAL n)))))) is set
- x0 is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
m + (- x0) is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
K708(REAL,REAL,(REAL n),(REAL n),m,(- x0)) is Relation-like REAL /\ REAL -defined K640((K635((REAL n)) /\ K635((REAL n)))) -valued Function-like V239() V240() V241() Element of K6(K7((REAL /\ REAL),K640((K635((REAL n)) /\ K635((REAL n))))))
dom (m - x0) is V160() V161() V162() Element of K6(REAL)
dom m is V160() V161() V162() Element of K6(REAL)
dom x0 is V160() V161() V162() Element of K6(REAL)
(dom m) /\ (dom x0) is V160() V161() V162() Element of K6(REAL)
dom (m + (- x0)) is V160() V161() V162() Element of K6(REAL)
dom (- x0) is V160() V161() V162() Element of K6(REAL)
(dom m) /\ (dom (- x0)) is V160() V161() V162() Element of K6(REAL)
S is set
x0 . S is Relation-like Function-like complex-valued ext-real-valued real-valued set
x0 /. S is Relation-like Function-like complex-valued ext-real-valued real-valued V56(n) Element of REAL n
(- x0) . S is Relation-like Function-like complex-valued ext-real-valued real-valued set
(- x0) /. S is Relation-like Function-like complex-valued ext-real-valued real-valued V56(n) Element of REAL n
(m - x0) . S is Relation-like Function-like complex-valued ext-real-valued real-valued set
m . S is Relation-like Function-like complex-valued ext-real-valued real-valued set
(m . S) - (x0 . S) is Relation-like Function-like complex-valued ext-real-valued real-valued set
- (x0 . S) is Relation-like Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (x0 . S) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(m . S) + (- (x0 . S)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(m . S) + ((- x0) . S) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(m + (- x0)) . S is Relation-like Function-like complex-valued ext-real-valued real-valued set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL n is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is set
K6(K7(REAL,(REAL n))) is set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL n is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is set
K6(K7(REAL,(REAL n))) is set
REAL-NS n is non empty non trivial V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() strict RealNormSpace-like V156() NORMSTR
the carrier of (REAL-NS n) is non empty non trivial set
K7(REAL, the carrier of (REAL-NS n)) is set
K6(K7(REAL, the carrier of (REAL-NS n))) is set
m is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
x0 is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
S is V11() real ext-real set
T is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL n is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is set
K6(K7(REAL,(REAL n))) is set
REAL-NS n is non empty non trivial V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() strict RealNormSpace-like V156() NORMSTR
the carrier of (REAL-NS n) is non empty non trivial set
K7(REAL, the carrier of (REAL-NS n)) is set
K6(K7(REAL, the carrier of (REAL-NS n))) is set
m is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
x0 is V11() real ext-real set
S is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
diff (S,x0) is Element of the carrier of (REAL-NS n)
g is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
S is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
diff (g,x0) is Element of the carrier of (REAL-NS n)
N1 is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
T is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
diff (N1,x0) is Element of the carrier of (REAL-NS n)
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL n is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is set
K6(K7(REAL,(REAL n))) is set
REAL-NS n is non empty non trivial V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() strict RealNormSpace-like V156() NORMSTR
the carrier of (REAL-NS n) is non empty non trivial set
K7(REAL, the carrier of (REAL-NS n)) is set
K6(K7(REAL, the carrier of (REAL-NS n))) is set
m is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
x0 is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
S is V11() real ext-real set
(n,m,S) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
diff (x0,S) is Element of the carrier of (REAL-NS n)
T is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
diff (T,S) is Element of the carrier of (REAL-NS n)
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL n is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is set
K6(K7(REAL,(REAL n))) is set
n is set
m is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL m is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL m)) is set
K6(K7(REAL,(REAL m))) is set
x0 is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
dom x0 is V160() V161() V162() Element of K6(REAL)
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL n is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is set
K6(K7(REAL,(REAL n))) is set
m is V160() V161() V162() open Element of K6(REAL)
x0 is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
dom x0 is V160() V161() V162() Element of K6(REAL)
REAL-NS n is non empty non trivial V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() strict RealNormSpace-like V156() NORMSTR
the carrier of (REAL-NS n) is non empty non trivial set
K7(REAL, the carrier of (REAL-NS n)) is set
K6(K7(REAL, the carrier of (REAL-NS n))) is set
S is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
dom S is V160() V161() V162() Element of K6(REAL)
T is V11() real ext-real Element of REAL
x0 | m is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
S | m is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
T is V11() real ext-real Element of REAL
T is V11() real ext-real Element of REAL
T is V11() real ext-real Element of REAL
S is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
T is V11() real ext-real Element of REAL
S | m is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
x0 | m is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL n is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is set
K6(K7(REAL,(REAL n))) is set
m is V160() V161() V162() Element of K6(REAL)
x0 is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
REAL-NS n is non empty non trivial V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() strict RealNormSpace-like V156() NORMSTR
the carrier of (REAL-NS n) is non empty non trivial set
K7(REAL, the carrier of (REAL-NS n)) is set
K6(K7(REAL, the carrier of (REAL-NS n))) is set
S is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
dom S is V160() V161() V162() Element of K6(REAL)
T is V11() real ext-real Element of REAL
x0 | m is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
S | m is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL n is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is set
K6(K7(REAL,(REAL n))) is set
m is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
x0 is set
S is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
dom S is V160() V161() V162() Element of K6(REAL)
T is set
T is set
T is V11() real ext-real Element of REAL
S . T is Relation-like Function-like complex-valued ext-real-valued real-valued set
(n,m,T) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
T is V11() real ext-real Element of REAL
S . T is Relation-like Function-like complex-valued ext-real-valued real-valued set
(n,m,T) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
S is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
dom S is V160() V161() V162() Element of K6(REAL)
T is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
dom T is V160() V161() V162() Element of K6(REAL)
g is V11() real ext-real Element of REAL
S . g is Relation-like Function-like complex-valued ext-real-valued real-valued set
(n,m,g) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
T . g is Relation-like Function-like complex-valued ext-real-valued real-valued set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL n is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is set
K6(K7(REAL,(REAL n))) is set
0* n is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
n |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of n -tuples_on REAL
m is V160() V161() V162() open Element of K6(REAL)
x0 is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
dom x0 is V160() V161() V162() Element of K6(REAL)
rng x0 is functional V233() V234() V235() Element of K6((REAL n))
K6((REAL n)) is set
(n,x0,m) is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
S is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
{S} is non empty functional V233() set
REAL-NS n is non empty non trivial V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() strict RealNormSpace-like V156() NORMSTR
the carrier of (REAL-NS n) is non empty non trivial set
K7(REAL, the carrier of (REAL-NS n)) is set
K6(K7(REAL, the carrier of (REAL-NS n))) is set
T is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
T `| m is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
0. (REAL-NS n) is V68( REAL-NS n) Element of the carrier of (REAL-NS n)
the ZeroF of (REAL-NS n) is Element of the carrier of (REAL-NS n)
g is V11() real ext-real Element of REAL
(T `| m) /. g is Element of the carrier of (REAL-NS n)
g is V11() real ext-real Element of REAL
T | m is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
x0 | m is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
g is V11() real ext-real Element of REAL
(T `| m) /. g is Element of the carrier of (REAL-NS n)
dom (T `| m) is V160() V161() V162() Element of K6(REAL)
(T `| m) . g is set
diff (T,g) is Element of the carrier of (REAL-NS n)
(n,x0,m) . g is Relation-like Function-like complex-valued ext-real-valued real-valued set
(n,x0,g) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
dom (n,x0,m) is V160() V161() V162() Element of K6(REAL)
(n,x0,m) /. g is Relation-like Function-like complex-valued ext-real-valued real-valued V56(n) Element of REAL n
g is V11() real ext-real Element of REAL
(n,x0,m) /. g is Relation-like Function-like complex-valued ext-real-valued real-valued V56(n) Element of REAL n
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL n is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is set
K6(K7(REAL,(REAL n))) is set
REAL-NS n is non empty non trivial V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() strict RealNormSpace-like V156() NORMSTR
the carrier of (REAL-NS n) is non empty non trivial set
K7(REAL, the carrier of (REAL-NS n)) is set
K6(K7(REAL, the carrier of (REAL-NS n))) is set
m is V11() real ext-real set
{m} is non empty V160() V161() V162() set
x0 is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
dom x0 is V160() V161() V162() Element of K6(REAL)
(n,x0,m) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
S is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
T is V160() V161() V162() open Neighbourhood of m
g is non empty Relation-like non-empty NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K6(K7(NAT,REAL))
g " is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
N1 is non empty Relation-like NAT -defined REAL -valued Function-like constant total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng N1 is trivial V160() V161() V162() Element of K6(REAL)
g + N1 is non empty Relation-like NAT -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
rng (g + N1) is V160() V161() V162() Element of K6(REAL)
S /* (g + N1) is non empty Relation-like NAT -defined the carrier of (REAL-NS n) -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of (REAL-NS n)))
K7(NAT, the carrier of (REAL-NS n)) is set
K6(K7(NAT, the carrier of (REAL-NS n))) is set
S /* N1 is non empty Relation-like NAT -defined the carrier of (REAL-NS n) -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of (REAL-NS n)))
(S /* (g + N1)) - (S /* N1) is non empty Relation-like NAT -defined the carrier of (REAL-NS n) -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of (REAL-NS n)))
(g ") (#) ((S /* (g + N1)) - (S /* N1)) is non empty Relation-like NAT -defined the carrier of (REAL-NS n) -valued Function-like total quasi_total Element of K6(K7(NAT, the carrier of (REAL-NS n)))
lim ((g ") (#) ((S /* (g + N1)) - (S /* N1))) is Element of the carrier of (REAL-NS n)
diff (S,m) is Element of the carrier of (REAL-NS n)
n is V11() real ext-real Element of REAL
m is V11() real ext-real Element of REAL
x0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL x0 is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
x0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL x0)) is set
K6(K7(REAL,(REAL x0))) is set
S is Relation-like REAL -defined REAL x0 -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL x0)))
m (#) S is Relation-like REAL -defined REAL x0 -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL x0)))
K677(REAL,(REAL x0),S,m) is Relation-like REAL -defined K640(K635((REAL x0))) -valued Function-like V239() V240() V241() Element of K6(K7(REAL,K640(K635((REAL x0)))))
K635((REAL x0)) is set
K640(K635((REAL x0))) is functional V233() V234() V235() set
K7(REAL,K640(K635((REAL x0)))) is set
K6(K7(REAL,K640(K635((REAL x0))))) is set
(x0,(m (#) S),n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(x0) FinSequence-like Element of REAL x0
(x0,S,n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(x0) FinSequence-like Element of REAL x0
m * (x0,S,n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(x0) FinSequence-like Element of REAL x0
K395(m) 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))
K450() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
id REAL is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one total quasi_total complex-valued ext-real-valued real-valued increasing non-decreasing Element of K6(K7(REAL,REAL))
K450() [;] (m,(id REAL)) is set
(x0,S,n) (#) K395(m) is Relation-like Function-like complex-valued ext-real-valued real-valued set
REAL-NS x0 is non empty non trivial V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() strict RealNormSpace-like V156() NORMSTR
the carrier of (REAL-NS x0) is non empty non trivial set
K7(REAL, the carrier of (REAL-NS x0)) is set
K6(K7(REAL, the carrier of (REAL-NS x0))) is set
T is Relation-like REAL -defined the carrier of (REAL-NS x0) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS x0)))
m (#) T is Relation-like REAL -defined the carrier of (REAL-NS x0) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS x0)))
diff ((m (#) T),n) is Element of the carrier of (REAL-NS x0)
diff (T,n) is Element of the carrier of (REAL-NS x0)
m * (diff (T,n)) is Element of the carrier of (REAL-NS x0)
the Mult of (REAL-NS x0) is Relation-like K7(REAL, the carrier of (REAL-NS x0)) -defined the carrier of (REAL-NS x0) -valued Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of (REAL-NS x0)), the carrier of (REAL-NS x0)))
K7(K7(REAL, the carrier of (REAL-NS x0)), the carrier of (REAL-NS x0)) is set
K6(K7(K7(REAL, the carrier of (REAL-NS x0)), the carrier of (REAL-NS x0))) is set
K466( the Mult of (REAL-NS x0),m,(diff (T,n))) is set
n is V11() real ext-real Element of REAL
m is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL m is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL m)) is set
K6(K7(REAL,(REAL m))) is set
x0 is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
- x0 is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
(m,(- x0),n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
(m,x0,n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
- (m,x0,n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
K446() 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))
(m,x0,n) (#) K446() is Relation-like Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (m,x0,n) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued FinSequence-like set
K395(K38(1)) 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))
K450() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
id REAL is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one total quasi_total complex-valued ext-real-valued real-valued increasing non-decreasing Element of K6(K7(REAL,REAL))
K450() [;] (K38(1),(id REAL)) is set
(m,x0,n) (#) K395(K38(1)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) x0 is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
K677(REAL,(REAL m),x0,(- 1)) is Relation-like REAL -defined K640(K635((REAL m))) -valued Function-like V239() V240() V241() Element of K6(K7(REAL,K640(K635((REAL m)))))
K635((REAL m)) is set
K640(K635((REAL m))) is functional V233() V234() V235() set
K7(REAL,K640(K635((REAL m)))) is set
K6(K7(REAL,K640(K635((REAL m))))) is set
n is V11() real ext-real Element of REAL
m is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL m is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL m)) is set
K6(K7(REAL,(REAL m))) is set
x0 is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
(m,x0,n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
S is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
x0 + S is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
K708(REAL,REAL,(REAL m),(REAL m),x0,S) is Relation-like REAL /\ REAL -defined K640((K635((REAL m)) /\ K635((REAL m)))) -valued Function-like V239() V240() V241() Element of K6(K7((REAL /\ REAL),K640((K635((REAL m)) /\ K635((REAL m))))))
REAL /\ REAL is V160() V161() V162() set
K635((REAL m)) is set
K635((REAL m)) /\ K635((REAL m)) is set
K640((K635((REAL m)) /\ K635((REAL m)))) is functional V233() V234() V235() set
K7((REAL /\ REAL),K640((K635((REAL m)) /\ K635((REAL m))))) is set
K6(K7((REAL /\ REAL),K640((K635((REAL m)) /\ K635((REAL m)))))) is set
(m,(x0 + S),n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
(m,S,n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
(m,x0,n) + (m,S,n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
K448() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
K448() .: ((m,x0,n),(m,S,n)) is set
REAL-NS m is non empty non trivial V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() strict RealNormSpace-like V156() NORMSTR
the carrier of (REAL-NS m) is non empty non trivial set
K7(REAL, the carrier of (REAL-NS m)) is set
K6(K7(REAL, the carrier of (REAL-NS m))) is set
T is Relation-like REAL -defined the carrier of (REAL-NS m) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS m)))
g is Relation-like REAL -defined the carrier of (REAL-NS m) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS m)))
T + g is Relation-like REAL -defined the carrier of (REAL-NS m) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS m)))
diff ((T + g),n) is Element of the carrier of (REAL-NS m)
diff (T,n) is Element of the carrier of (REAL-NS m)
diff (g,n) is Element of the carrier of (REAL-NS m)
(diff (T,n)) + (diff (g,n)) is Element of the carrier of (REAL-NS m)
n is V11() real ext-real Element of REAL
m is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL m is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL m)) is set
K6(K7(REAL,(REAL m))) is set
x0 is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
(m,x0,n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
S is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
x0 - S is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
K714(REAL,REAL,(REAL m),(REAL m),x0,S) is Relation-like REAL /\ REAL -defined K640((K635((REAL m)) /\ K635((REAL m)))) -valued Function-like V239() V240() V241() Element of K6(K7((REAL /\ REAL),K640((K635((REAL m)) /\ K635((REAL m))))))
REAL /\ REAL is V160() V161() V162() set
K635((REAL m)) is set
K635((REAL m)) /\ K635((REAL m)) is set
K640((K635((REAL m)) /\ K635((REAL m)))) is functional V233() V234() V235() set
K7((REAL /\ REAL),K640((K635((REAL m)) /\ K635((REAL m))))) is set
K6(K7((REAL /\ REAL),K640((K635((REAL m)) /\ K635((REAL m)))))) is set
(m,(x0 - S),n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
(m,S,n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
(m,x0,n) - (m,S,n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
K449() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
K448() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
id REAL is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one total quasi_total complex-valued ext-real-valued real-valued increasing non-decreasing Element of K6(K7(REAL,REAL))
K446() 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))
K448() * ((id REAL),K446()) is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
K449() .: ((m,x0,n),(m,S,n)) is set
- (m,S,n) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued FinSequence-like set
(m,S,n) (#) K446() is Relation-like Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (m,S,n) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued FinSequence-like set
K395(K38(1)) 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))
K450() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
K450() [;] (K38(1),(id REAL)) is set
(m,S,n) (#) K395(K38(1)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(m,x0,n) + (- (m,S,n)) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued FinSequence-like set
K448() .: ((m,x0,n),(- (m,S,n))) is set
- S is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
x0 + (- S) is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
K708(REAL,REAL,(REAL m),(REAL m),x0,(- S)) is Relation-like REAL /\ REAL -defined K640((K635((REAL m)) /\ K635((REAL m)))) -valued Function-like V239() V240() V241() Element of K6(K7((REAL /\ REAL),K640((K635((REAL m)) /\ K635((REAL m))))))
(m,(- S),n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
- (m,S,n) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
n is V11() real ext-real Element of REAL
m is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL m is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
m -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL m)) is set
K6(K7(REAL,(REAL m))) is set
x0 is V160() V161() V162() open Element of K6(REAL)
S is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
dom S is V160() V161() V162() Element of K6(REAL)
n (#) S is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
K677(REAL,(REAL m),S,n) is Relation-like REAL -defined K640(K635((REAL m))) -valued Function-like V239() V240() V241() Element of K6(K7(REAL,K640(K635((REAL m)))))
K635((REAL m)) is set
K640(K635((REAL m))) is functional V233() V234() V235() set
K7(REAL,K640(K635((REAL m)))) is set
K6(K7(REAL,K640(K635((REAL m))))) is set
(m,(n (#) S),x0) is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
REAL-NS m is non empty non trivial V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() strict RealNormSpace-like V156() NORMSTR
the carrier of (REAL-NS m) is non empty non trivial set
K7(REAL, the carrier of (REAL-NS m)) is set
K6(K7(REAL, the carrier of (REAL-NS m))) is set
dom (n (#) S) is V160() V161() V162() Element of K6(REAL)
T is Relation-like REAL -defined the carrier of (REAL-NS m) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS m)))
n (#) T is Relation-like REAL -defined the carrier of (REAL-NS m) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS m)))
dom (n (#) T) is V160() V161() V162() Element of K6(REAL)
dom T is V160() V161() V162() Element of K6(REAL)
g is V11() real ext-real Element of REAL
S | x0 is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
T | x0 is Relation-like REAL -defined the carrier of (REAL-NS m) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS m)))
(n (#) T) `| x0 is Relation-like REAL -defined the carrier of (REAL-NS m) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS m)))
g is V11() real ext-real Element of REAL
((n (#) T) `| x0) . g is set
diff (T,g) is Element of the carrier of (REAL-NS m)
n * (diff (T,g)) is Element of the carrier of (REAL-NS m)
the Mult of (REAL-NS m) is Relation-like K7(REAL, the carrier of (REAL-NS m)) -defined the carrier of (REAL-NS m) -valued Function-like total quasi_total Element of K6(K7(K7(REAL, the carrier of (REAL-NS m)), the carrier of (REAL-NS m)))
K7(K7(REAL, the carrier of (REAL-NS m)), the carrier of (REAL-NS m)) is set
K6(K7(K7(REAL, the carrier of (REAL-NS m)), the carrier of (REAL-NS m))) is set
K466( the Mult of (REAL-NS m),n,(diff (T,g))) is set
g is V11() real ext-real Element of REAL
(n (#) T) | x0 is Relation-like REAL -defined the carrier of (REAL-NS m) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS m)))
(n (#) S) | x0 is Relation-like REAL -defined REAL m -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL m)))
g is V11() real ext-real Element of REAL
(m,(n (#) S),g) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
(m,S,g) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
n * (m,S,g) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
K395(n) 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))
K450() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
id REAL is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one total quasi_total complex-valued ext-real-valued real-valued increasing non-decreasing Element of K6(K7(REAL,REAL))
K450() [;] (n,(id REAL)) is set
(m,S,g) (#) K395(n) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(m,(n (#) S),x0) . g is Relation-like Function-like complex-valued ext-real-valued real-valued set
g is V11() real ext-real Element of REAL
(m,(n (#) S),x0) . g is Relation-like Function-like complex-valued ext-real-valued real-valued set
(m,S,g) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
n * (m,S,g) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(m) FinSequence-like Element of REAL m
(m,S,g) (#) K395(n) is Relation-like Function-like complex-valued ext-real-valued real-valued set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL n is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is set
K6(K7(REAL,(REAL n))) is set
m is V160() V161() V162() open Element of K6(REAL)
x0 is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
dom x0 is V160() V161() V162() Element of K6(REAL)
- x0 is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
(n,(- x0),m) is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
(- 1) (#) x0 is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
K677(REAL,(REAL n),x0,(- 1)) is Relation-like REAL -defined K640(K635((REAL n))) -valued Function-like V239() V240() V241() Element of K6(K7(REAL,K640(K635((REAL n)))))
K635((REAL n)) is set
K640(K635((REAL n))) is functional V233() V234() V235() set
K7(REAL,K640(K635((REAL n)))) is set
K6(K7(REAL,K640(K635((REAL n))))) is set
S is V11() real ext-real Element of REAL
(n,(- x0),m) . S is Relation-like Function-like complex-valued ext-real-valued real-valued set
(n,x0,S) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
- (n,x0,S) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
K446() 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))
(n,x0,S) (#) K446() is Relation-like Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (n,x0,S) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued FinSequence-like set
K395(K38(1)) 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))
K450() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
id REAL is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one total quasi_total complex-valued ext-real-valued real-valued increasing non-decreasing Element of K6(K7(REAL,REAL))
K450() [;] (K38(1),(id REAL)) is set
(n,x0,S) (#) K395(K38(1)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL n is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is set
K6(K7(REAL,(REAL n))) is set
m is V160() V161() V162() open Element of K6(REAL)
x0 is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
S is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
x0 + S is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
K708(REAL,REAL,(REAL n),(REAL n),x0,S) is Relation-like REAL /\ REAL -defined K640((K635((REAL n)) /\ K635((REAL n)))) -valued Function-like V239() V240() V241() Element of K6(K7((REAL /\ REAL),K640((K635((REAL n)) /\ K635((REAL n))))))
REAL /\ REAL is V160() V161() V162() set
K635((REAL n)) is set
K635((REAL n)) /\ K635((REAL n)) is set
K640((K635((REAL n)) /\ K635((REAL n)))) is functional V233() V234() V235() set
K7((REAL /\ REAL),K640((K635((REAL n)) /\ K635((REAL n))))) is set
K6(K7((REAL /\ REAL),K640((K635((REAL n)) /\ K635((REAL n)))))) is set
dom (x0 + S) is V160() V161() V162() Element of K6(REAL)
(n,(x0 + S),m) is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
REAL-NS n is non empty non trivial V87() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V122() V123() strict RealNormSpace-like V156() NORMSTR
the carrier of (REAL-NS n) is non empty non trivial set
K7(REAL, the carrier of (REAL-NS n)) is set
K6(K7(REAL, the carrier of (REAL-NS n))) is set
T is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
g is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
T + g is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
dom (T + g) is V160() V161() V162() Element of K6(REAL)
dom T is V160() V161() V162() Element of K6(REAL)
dom g is V160() V161() V162() Element of K6(REAL)
N1 is V11() real ext-real Element of REAL
x0 | m is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
T | m is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
N1 is V11() real ext-real Element of REAL
S | m is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
g | m is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
(T + g) `| m is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
N1 is V11() real ext-real Element of REAL
((T + g) `| m) . N1 is set
diff (T,N1) is Element of the carrier of (REAL-NS n)
diff (g,N1) is Element of the carrier of (REAL-NS n)
(diff (T,N1)) + (diff (g,N1)) is Element of the carrier of (REAL-NS n)
N1 is V11() real ext-real Element of REAL
(T + g) | m is Relation-like REAL -defined the carrier of (REAL-NS n) -valued Function-like Element of K6(K7(REAL, the carrier of (REAL-NS n)))
(x0 + S) | m is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
N1 is V11() real ext-real Element of REAL
(n,(x0 + S),m) . N1 is Relation-like Function-like complex-valued ext-real-valued real-valued set
(n,x0,N1) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
(n,S,N1) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
(n,x0,N1) + (n,S,N1) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
K448() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
K448() .: ((n,x0,N1),(n,S,N1)) is set
(n,(x0 + S),N1) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL n is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is set
K6(K7(REAL,(REAL n))) is set
m is V160() V161() V162() open Element of K6(REAL)
x0 is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
S is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
x0 - S is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
K714(REAL,REAL,(REAL n),(REAL n),x0,S) is Relation-like REAL /\ REAL -defined K640((K635((REAL n)) /\ K635((REAL n)))) -valued Function-like V239() V240() V241() Element of K6(K7((REAL /\ REAL),K640((K635((REAL n)) /\ K635((REAL n))))))
REAL /\ REAL is V160() V161() V162() set
K635((REAL n)) is set
K635((REAL n)) /\ K635((REAL n)) is set
K640((K635((REAL n)) /\ K635((REAL n)))) is functional V233() V234() V235() set
K7((REAL /\ REAL),K640((K635((REAL n)) /\ K635((REAL n))))) is set
K6(K7((REAL /\ REAL),K640((K635((REAL n)) /\ K635((REAL n)))))) is set
dom (x0 - S) is V160() V161() V162() Element of K6(REAL)
(n,(x0 - S),m) is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
- S is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
x0 + (- S) is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
K708(REAL,REAL,(REAL n),(REAL n),x0,(- S)) is Relation-like REAL /\ REAL -defined K640((K635((REAL n)) /\ K635((REAL n)))) -valued Function-like V239() V240() V241() Element of K6(K7((REAL /\ REAL),K640((K635((REAL n)) /\ K635((REAL n))))))
dom x0 is V160() V161() V162() Element of K6(REAL)
dom S is V160() V161() V162() Element of K6(REAL)
(dom x0) /\ (dom S) is V160() V161() V162() Element of K6(REAL)
T is V11() real ext-real Element of REAL
(n,(x0 - S),m) . T is Relation-like Function-like complex-valued ext-real-valued real-valued set
(n,x0,T) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
(n,S,T) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
(n,x0,T) - (n,S,T) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
K449() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
K448() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
id REAL is non empty Relation-like REAL -defined REAL -valued Function-like one-to-one total quasi_total complex-valued ext-real-valued real-valued increasing non-decreasing Element of K6(K7(REAL,REAL))
K446() 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))
K448() * ((id REAL),K446()) is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
K449() .: ((n,x0,T),(n,S,T)) is set
- (n,S,T) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued FinSequence-like set
(n,S,T) (#) K446() is Relation-like Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real non positive set
K38(1) (#) (n,S,T) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued FinSequence-like set
K395(K38(1)) 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))
K450() is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(K7(REAL,REAL),REAL))
K450() [;] (K38(1),(id REAL)) is set
(n,S,T) (#) K395(K38(1)) is Relation-like Function-like complex-valued ext-real-valued real-valued set
(n,x0,T) + (- (n,S,T)) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued FinSequence-like set
K448() .: ((n,x0,T),(- (n,S,T))) is set
(n,(- S),T) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
(n,x0,T) + (n,(- S),T) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
K448() .: ((n,x0,T),(n,(- S),T)) is set
n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V132() V159() V160() V161() V162() V163() V164() V165() Element of NAT
REAL n is non empty functional FinSequence-membered V233() V234() V235() FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(REAL,(REAL n)) is set
K6(K7(REAL,(REAL n))) is set
0* n is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of REAL n
n |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V56(n) FinSequence-like Element of n -tuples_on REAL
m is V160() V161() V162() open Element of K6(REAL)
x0 is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
dom x0 is V160() V161() V162() Element of K6(REAL)
x0 | m is Relation-like REAL -defined REAL n -valued Function-like V239() V240() V241() Element of K6(K7(REAL,(REAL n)))
(n,x0,m) is Relation-like REAL