:: NDIFF_4 semantic presentation

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