REAL is non empty V2() V32() V129() V130() V131() V135() V160() V161() V163() set
NAT is non empty V2() epsilon-transitive epsilon-connected ordinal V32() V37() V38() V129() V130() V131() V132() V133() V134() V135() V158() V160() Element of K6(REAL)
K6(REAL) is V2() V32() set
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
K7(NAT,(REAL *)) is V2() Relation-like V32() set
K6(K7(NAT,(REAL *))) is V2() V32() set
omega is non empty V2() epsilon-transitive epsilon-connected ordinal V32() V37() V38() V129() V130() V131() V132() V133() V134() V135() V158() V160() set
K6(omega) is V2() V32() set
K6(NAT) is V2() V32() set
COMPLEX is non empty V2() V32() V129() V135() set
RAT is non empty V2() V32() V129() V130() V131() V132() V135() set
INT is non empty V2() V32() V129() V130() V131() V132() V133() V135() set
K7(REAL,REAL) is V2() Relation-like V32() complex-valued ext-real-valued real-valued set
K6(K7(REAL,REAL)) is V2() V32() set
K316() is non empty V75() L8()
the carrier of K316() is non empty set
K321() is non empty L8()
K322() is non empty V75() M13(K321())
K323() is non empty V75() V97() V157() M16(K321(),K322())
K325() is non empty V75() V97() V99() V101() L8()
K326() is non empty V75() V97() V157() M13(K325())
K7(COMPLEX,COMPLEX) is V2() Relation-like V32() complex-valued set
K6(K7(COMPLEX,COMPLEX)) is V2() V32() set
K7(COMPLEX,REAL) is V2() Relation-like V32() complex-valued ext-real-valued real-valued set
K6(K7(COMPLEX,REAL)) is V2() V32() set
K7(NAT,REAL) is V2() Relation-like V32() complex-valued ext-real-valued real-valued set
K6(K7(NAT,REAL)) is V2() V32() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() V158() V159() V160() V161() V162() Element of NAT
K7(1,1) is Relation-like RAT -valued INT -valued V32() complex-valued ext-real-valued real-valued natural-valued set
K6(K7(1,1)) is V32() V36() set
K7(K7(1,1),1) is Relation-like RAT -valued INT -valued V32() complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(1,1),1)) is V32() V36() set
K7(K7(1,1),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(K7(1,1),REAL)) is set
K7(K7(REAL,REAL),REAL) is V2() Relation-like V32() complex-valued ext-real-valued real-valued set
K6(K7(K7(REAL,REAL),REAL)) is V2() V32() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() V158() V159() V160() V161() V162() Element of NAT
K7(2,2) is Relation-like RAT -valued INT -valued V32() complex-valued ext-real-valued real-valued natural-valued set
K7(K7(2,2),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(K7(2,2),REAL)) is set
TOP-REAL 2 is non empty V73() V142() V168() V169() V170() V171() V172() V173() V174() TopSpace-like V219() L20()
the carrier of (TOP-REAL 2) is non empty set
REAL 1 is non empty functional FinSequence-membered V255() V256() V257() FinSequenceSet of REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = 1 } is set
K7((REAL 1),(REAL 1)) is Relation-like set
K6(K7((REAL 1),(REAL 1))) is set
REAL-NS 1 is non empty V52() V73() V168() V169() V170() V171() V172() V173() V174() V178() V179() strict RealNormSpace-like V187() NORMSTR
the carrier of (REAL-NS 1) is non empty V2() set
K436((REAL-NS 1),(REAL-NS 1)) is non empty NORMSTR
the carrier of K436((REAL-NS 1),(REAL-NS 1)) is non empty set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V2() Relation-like V32() complex-valued set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is V2() V32() set
K7(RAT,RAT) is V2() Relation-like RAT -valued V32() complex-valued ext-real-valued real-valued set
K6(K7(RAT,RAT)) is V2() V32() set
K7(K7(RAT,RAT),RAT) is V2() Relation-like RAT -valued V32() complex-valued ext-real-valued real-valued set
K6(K7(K7(RAT,RAT),RAT)) is V2() V32() set
K7(INT,INT) is V2() Relation-like RAT -valued INT -valued V32() complex-valued ext-real-valued real-valued set
K6(K7(INT,INT)) is V2() V32() set
K7(K7(INT,INT),INT) is V2() Relation-like RAT -valued INT -valued V32() complex-valued ext-real-valued real-valued set
K6(K7(K7(INT,INT),INT)) is V2() V32() set
K7(NAT,NAT) is V2() Relation-like RAT -valued INT -valued V32() complex-valued ext-real-valued real-valued natural-valued set
K7(K7(NAT,NAT),NAT) is V2() Relation-like RAT -valued INT -valued V32() complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(NAT,NAT),NAT)) is V2() V32() set
ExtREAL is non empty V130() V163() set
the_set_of_RealSequences is non empty set
K7(the_set_of_RealSequences,the_set_of_RealSequences) is Relation-like set
K7(K7(the_set_of_RealSequences,the_set_of_RealSequences),the_set_of_RealSequences) is Relation-like set
K6(K7(K7(the_set_of_RealSequences,the_set_of_RealSequences),the_set_of_RealSequences)) is set
K7(REAL,the_set_of_RealSequences) is V2() Relation-like V32() set
K7(K7(REAL,the_set_of_RealSequences),the_set_of_RealSequences) is V2() Relation-like V32() set
K6(K7(K7(REAL,the_set_of_RealSequences),the_set_of_RealSequences)) is V2() V32() set
Linear_Space_of_RealSequences is L13()
the carrier of Linear_Space_of_RealSequences is set
K6( the carrier of Linear_Space_of_RealSequences) is set
the_set_of_l2RealSequences is Element of K6( the carrier of Linear_Space_of_RealSequences)
K7(the_set_of_l2RealSequences,the_set_of_l2RealSequences) is Relation-like set
K7(K7(the_set_of_l2RealSequences,the_set_of_l2RealSequences),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(K7(the_set_of_l2RealSequences,the_set_of_l2RealSequences),REAL)) is set
K682() is Element of K6( the carrier of Linear_Space_of_RealSequences)
K7(K682(),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(K682(),REAL)) is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V36() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V129() V130() V131() V132() V133() V134() V135() V160() V161() V162() V163() V255() V256() V257() V258() V259() V260() V261() V262() V263() V264() V265() V266() bounded set
{{},1} is non empty V32() V36() V129() V130() V131() V132() V133() V134() V158() V159() V160() V161() V162() set
K200() is V96() L11()
the carrier of K200() is set
the carrier of K200() * is non empty functional FinSequence-membered FinSequenceSet of the carrier of K200()
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional V32() V33() V36() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V44() V45() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V129() V130() V131() V132() V133() V134() V135() V160() V161() V162() V163() V255() V256() V257() V258() V259() V260() V261() V262() V263() V264() V265() V266() bounded Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() V158() V159() V160() V161() V162() Element of NAT
- 1 is V11() real ext-real non positive Element of REAL
Seg 1 is non empty V2() V32() V39(1) V129() V130() V131() V132() V133() V134() V158() V159() V160() V161() V162() Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty V2() V32() V36() V39(1) V129() V130() V131() V132() V133() V134() V158() V159() V160() V161() V162() set
Seg 2 is non empty V32() V39(2) V129() V130() V131() V132() V133() V134() V158() V159() V160() V161() V162() Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty V32() V36() V129() V130() V131() V132() V133() V134() V158() V159() V160() V161() V162() set
<*> REAL is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional V32() V33() V36() V37() V39( {} ) FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V129() V130() V131() V132() V133() V134() V135() V160() V161() V162() V163() V255() V256() V257() V258() V259() V260() V261() V262() V263() V264() V265() V266() bounded FinSequence of REAL
Sum (<*> REAL) is V11() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
REAL a is non empty functional FinSequence-membered V255() V256() V257() FinSequenceSet of REAL
a -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = a } is set
K7(REAL,(REAL a)) is V2() Relation-like V32() set
K6(K7(REAL,(REAL a))) is V2() V32() set
b is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
x0 is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
b - x0 is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
K777(REAL,REAL,(REAL a),(REAL a),b,x0) is Relation-like REAL /\ REAL -defined K703((K698((REAL a)) /\ K698((REAL a)))) -valued Function-like V261() V262() V263() Element of K6(K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a))))))
REAL /\ REAL is V129() V130() V131() V163() set
K698((REAL a)) is set
K698((REAL a)) /\ K698((REAL a)) is set
K703((K698((REAL a)) /\ K698((REAL a)))) is functional V255() V256() V257() set
K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a))))) is Relation-like set
K6(K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a)))))) is set
- x0 is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
b + (- x0) is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
K771(REAL,REAL,(REAL a),(REAL a),b,(- x0)) is Relation-like REAL /\ REAL -defined K703((K698((REAL a)) /\ K698((REAL a)))) -valued Function-like V261() V262() V263() Element of K6(K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a))))))
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
x0 is V11() real ext-real set
['a,x0'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
['b,x0'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
[.a,x0.] is V129() V130() V131() V163() closed Element of K6(REAL)
{ b1 where b1 is V11() real ext-real Element of REAL : ( a <= b1 & b1 <= x0 ) } is set
[.b,x0.] is V129() V130() V131() V163() closed Element of K6(REAL)
{ b1 where b1 is V11() real ext-real Element of REAL : ( b <= b1 & b1 <= x0 ) } is set
[.a,b.] is V129() V130() V131() V163() closed Element of K6(REAL)
{ b1 where b1 is V11() real ext-real Element of REAL : ( a <= b1 & b1 <= b ) } is set
a is set
b is V11() real ext-real set
x0 is V11() real ext-real set
n is V11() real ext-real set
['x0,n'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
f is V11() real ext-real set
['b,f'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
['x0,f'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
x0 is V11() real ext-real set
n is V11() real ext-real set
min (x0,n) is V11() real ext-real set
max (x0,n) is V11() real ext-real set
['(min (x0,n)),(max (x0,n))'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
[.a,b.] is V129() V130() V131() V163() closed Element of K6(REAL)
{ b1 where b1 is V11() real ext-real Element of REAL : ( a <= b1 & b1 <= b ) } is set
['x0,b'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
['x0,n'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
['n,b'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
['n,x0'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
a is set
b is V11() real ext-real set
x0 is V11() real ext-real set
['b,x0'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
n is V11() real ext-real set
f is V11() real ext-real set
min (n,f) is V11() real ext-real set
max (n,f) is V11() real ext-real set
['(min (n,f)),(max (n,f))'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
a is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
REAL a is non empty functional FinSequence-membered V255() V256() V257() FinSequenceSet of REAL
a -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = a } is set
K7(REAL,(REAL a)) is V2() Relation-like V32() set
K6(K7(REAL,(REAL a))) is V2() V32() set
b is V11() real ext-real set
x0 is V11() real ext-real set
n is V11() real ext-real set
['x0,n'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
f is V11() real ext-real set
['b,f'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
F is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
dom F is V129() V130() V131() Element of K6(REAL)
c7 is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
dom c7 is V129() V130() V131() Element of K6(REAL)
F + c7 is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
K771(REAL,REAL,(REAL a),(REAL a),F,c7) is Relation-like REAL /\ REAL -defined K703((K698((REAL a)) /\ K698((REAL a)))) -valued Function-like V261() V262() V263() Element of K6(K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a))))))
REAL /\ REAL is V129() V130() V131() V163() set
K698((REAL a)) is set
K698((REAL a)) /\ K698((REAL a)) is set
K703((K698((REAL a)) /\ K698((REAL a)))) is functional V255() V256() V257() set
K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a))))) is Relation-like set
K6(K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a)))))) is set
dom (F + c7) is V129() V130() V131() Element of K6(REAL)
(dom F) /\ (dom c7) is V129() V130() V131() Element of K6(REAL)
['b,f'] /\ ['b,f'] is V129() V130() V131() V163() Element of K6(REAL)
a is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
REAL a is non empty functional FinSequence-membered V255() V256() V257() FinSequenceSet of REAL
a -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = a } is set
K7(REAL,(REAL a)) is V2() Relation-like V32() set
K6(K7(REAL,(REAL a))) is V2() V32() set
b is V11() real ext-real set
x0 is V11() real ext-real set
n is V11() real ext-real set
['x0,n'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
f is V11() real ext-real set
['b,f'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
F is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
dom F is V129() V130() V131() Element of K6(REAL)
c7 is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
dom c7 is V129() V130() V131() Element of K6(REAL)
F - c7 is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
K777(REAL,REAL,(REAL a),(REAL a),F,c7) is Relation-like REAL /\ REAL -defined K703((K698((REAL a)) /\ K698((REAL a)))) -valued Function-like V261() V262() V263() Element of K6(K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a))))))
REAL /\ REAL is V129() V130() V131() V163() set
K698((REAL a)) is set
K698((REAL a)) /\ K698((REAL a)) is set
K703((K698((REAL a)) /\ K698((REAL a)))) is functional V255() V256() V257() set
K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a))))) is Relation-like set
K6(K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a)))))) is set
dom (F - c7) is V129() V130() V131() Element of K6(REAL)
(dom F) /\ (dom c7) is V129() V130() V131() Element of K6(REAL)
['b,f'] /\ ['b,f'] is V129() V130() V131() V163() Element of K6(REAL)
a is non empty set
b is non empty set
K7(a,b) is Relation-like set
K6(K7(a,b)) is set
x0 is non empty set
K7(x0,b) is Relation-like set
K6(K7(x0,b)) is set
n is Relation-like a -defined b -valued Function-like Element of K6(K7(a,b))
dom n is Element of K6(a)
K6(a) is set
n | x0 is Relation-like a -defined x0 -defined a -defined b -valued Function-like Element of K6(K7(a,b))
rng n is Element of K6(b)
K6(b) is set
K7((dom n),b) is Relation-like set
K6(K7((dom n),b)) is set
a is V11() real ext-real set
b is V11() real ext-real set
x0 is V11() real ext-real set
['b,x0'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
n is V11() real ext-real set
['a,n'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
f is V11() real ext-real set
F is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
F | ['a,n'] is Relation-like REAL -defined ['a,n'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom F is V129() V130() V131() Element of K6(REAL)
f (#) F is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(f (#) F) | ['b,x0'] is Relation-like REAL -defined ['b,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
F | ['b,x0'] is Relation-like REAL -defined ['b,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
a is V11() real ext-real set
b is V11() real ext-real set
x0 is V11() real ext-real set
['b,x0'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
n is V11() real ext-real set
['a,n'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
F is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
f | ['a,n'] is Relation-like REAL -defined ['a,n'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
F | ['a,n'] is Relation-like REAL -defined ['a,n'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is V129() V130() V131() Element of K6(REAL)
dom F is V129() V130() V131() Element of K6(REAL)
f - F is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
- F is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
K38(1) is V11() real ext-real non positive set
K38(1) (#) F is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
f + (- F) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(f - F) | ['b,x0'] is Relation-like REAL -defined ['b,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
- 1 is V11() real V44() V45() ext-real non positive Element of INT
(- 1) (#) F is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((- 1) (#) F) | ['a,n'] is Relation-like REAL -defined ['a,n'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom ((- 1) (#) F) is V129() V130() V131() Element of K6(REAL)
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
x0 is V11() real ext-real set
n is V11() real ext-real set
min (x0,n) is V11() real ext-real set
max (x0,n) is V11() real ext-real set
['(min (x0,n)),(max (x0,n))'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
n - x0 is V11() real ext-real Element of REAL
abs (n - x0) is V11() real ext-real Element of REAL
f is V11() real ext-real set
f * (abs (n - x0)) is V11() real ext-real Element of REAL
F is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
F | ['a,b'] is Relation-like REAL -defined ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom F is V129() V130() V131() Element of K6(REAL)
integral (F,x0,n) is V11() real ext-real Element of REAL
abs (integral (F,x0,n)) is V11() real ext-real Element of REAL
abs F is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_below Element of K6(K7(REAL,REAL))
rng (abs F) is V129() V130() V131() Element of K6(REAL)
dom (abs F) is V129() V130() V131() Element of K6(REAL)
K7((dom (abs F)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7((dom (abs F)),REAL)) is set
K7(['(min (x0,n)),(max (x0,n))'],REAL) is V2() Relation-like V32() complex-valued ext-real-valued real-valued set
K6(K7(['(min (x0,n)),(max (x0,n))'],REAL)) is V2() V32() set
(abs F) | ['(min (x0,n)),(max (x0,n))'] is Relation-like REAL -defined ['(min (x0,n)),(max (x0,n))'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_below Element of K6(K7(REAL,REAL))
vol ['(min (x0,n)),(max (x0,n))'] is V11() real ext-real Element of REAL
x is non empty Relation-like ['(min (x0,n)),(max (x0,n))'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(['(min (x0,n)),(max (x0,n))'],REAL))
{f} is non empty V2() V32() V39(1) V129() V130() V131() V158() V159() V160() V161() V162() set
R is non empty Relation-like ['(min (x0,n)),(max (x0,n))'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(['(min (x0,n)),(max (x0,n))'],REAL))
rng R is non empty V129() V130() V131() Element of K6(REAL)
R | ['(min (x0,n)),(max (x0,n))'] is Relation-like ['(min (x0,n)),(max (x0,n))'] -defined ['(min (x0,n)),(max (x0,n))'] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['(min (x0,n)),(max (x0,n))'],REAL))
R is V11() real ext-real Element of REAL
x . R is V11() real ext-real Element of REAL
(abs F) . R is V11() real ext-real Element of REAL
F . R is V11() real ext-real Element of REAL
abs (F . R) is V11() real ext-real Element of REAL
R . R is V11() real ext-real Element of REAL
integral ((abs F),(min (x0,n)),(max (x0,n))) is V11() real ext-real Element of REAL
integral ((abs F),['(min (x0,n)),(max (x0,n))']) is V11() real ext-real Element of REAL
K576((abs F),['(min (x0,n)),(max (x0,n))']) is Relation-like ['(min (x0,n)),(max (x0,n))'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_below Element of K6(K7(['(min (x0,n)),(max (x0,n))'],REAL))
integral K576((abs F),['(min (x0,n)),(max (x0,n))']) is V11() real ext-real Element of REAL
x | ['(min (x0,n)),(max (x0,n))'] is Relation-like ['(min (x0,n)),(max (x0,n))'] -defined ['(min (x0,n)),(max (x0,n))'] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['(min (x0,n)),(max (x0,n))'],REAL))
integral R is V11() real ext-real Element of REAL
f * (vol ['(min (x0,n)),(max (x0,n))']) is V11() real ext-real Element of REAL
a is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom b is V129() V130() V131() Element of K6(REAL)
b | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
K7(a,REAL) is V2() Relation-like V32() complex-valued ext-real-valued real-valued set
K6(K7(a,REAL)) is V2() V32() set
a is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
REAL a is non empty functional FinSequence-membered V255() V256() V257() FinSequenceSet of REAL
a -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = a } is set
K7(REAL,(REAL a)) is V2() Relation-like V32() set
K6(K7(REAL,(REAL a))) is V2() V32() set
b is V11() real ext-real set
x0 is V11() real ext-real set
['b,x0'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
n is V11() real ext-real set
['b,n'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
['n,x0'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
f is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
f | ['b,x0'] is Relation-like REAL -defined ['b,x0'] -defined REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
dom f is V129() V130() V131() Element of K6(REAL)
integral (f,b,x0) is Relation-like NAT -defined REAL -valued Function-like V32() V39(a) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL a
integral (f,b,n) is Relation-like NAT -defined REAL -valued Function-like V32() V39(a) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL a
integral (f,n,x0) is Relation-like NAT -defined REAL -valued Function-like V32() V39(a) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL a
(integral (f,b,n)) + (integral (f,n,x0)) is Relation-like NAT -defined REAL -valued Function-like V32() V39(a) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL a
F is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
proj (F,a) is non empty Relation-like REAL a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL a),REAL))
K7((REAL a),REAL) is V2() Relation-like V32() complex-valued ext-real-valued real-valued set
K6(K7((REAL a),REAL)) is V2() V32() set
Seg a is V32() V39(a) V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT : ( 1 <= b1 & b1 <= a ) } is set
(proj (F,a)) * f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (F,a)) * (f | ['b,x0']) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((proj (F,a)) * f) | ['b,x0'] is Relation-like REAL -defined ['b,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (proj (F,a)) is non empty functional FinSequence-membered V255() V256() V257() Element of K6((REAL a))
K6((REAL a)) is set
rng f is functional FinSequence-membered V255() V256() V257() Element of K6((REAL a))
dom ((proj (F,a)) * f) is V129() V130() V131() Element of K6(REAL)
integral (((proj (F,a)) * f),b,x0) is V11() real ext-real Element of REAL
integral (((proj (F,a)) * f),b,n) is V11() real ext-real Element of REAL
integral (((proj (F,a)) * f),n,x0) is V11() real ext-real Element of REAL
(integral (((proj (F,a)) * f),b,n)) + (integral (((proj (F,a)) * f),n,x0)) is V11() real ext-real Element of REAL
F is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
proj (F,a) is non empty Relation-like REAL a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL a),REAL))
(proj (F,a)) * f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
F is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
proj (F,a) is non empty Relation-like REAL a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL a),REAL))
(proj (F,a)) * f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
F is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
dom (integral (f,b,x0)) is V32() V39(a) V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of K6(NAT)
proj (F,a) is non empty Relation-like REAL a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL a),REAL))
(integral (f,b,x0)) . F is V11() real ext-real Element of REAL
(proj (F,a)) * f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral (((proj (F,a)) * f),b,x0) is V11() real ext-real Element of REAL
integral (((proj (F,a)) * f),b,n) is V11() real ext-real Element of REAL
integral (((proj (F,a)) * f),n,x0) is V11() real ext-real Element of REAL
(integral (((proj (F,a)) * f),b,n)) + (integral (((proj (F,a)) * f),n,x0)) is V11() real ext-real Element of REAL
(integral (f,b,n)) . F is V11() real ext-real Element of REAL
((integral (f,b,n)) . F) + (integral (((proj (F,a)) * f),n,x0)) is V11() real ext-real Element of REAL
(integral (f,n,x0)) . F is V11() real ext-real Element of REAL
((integral (f,b,n)) . F) + ((integral (f,n,x0)) . F) is V11() real ext-real Element of REAL
((integral (f,b,n)) + (integral (f,n,x0))) . F is V11() real ext-real Element of REAL
len ((integral (f,b,n)) + (integral (f,n,x0))) is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
dom ((integral (f,b,n)) + (integral (f,n,x0))) is V32() V39(a) V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of K6(NAT)
a is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
REAL a is non empty functional FinSequence-membered V255() V256() V257() FinSequenceSet of REAL
a -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = a } is set
K7(REAL,(REAL a)) is V2() Relation-like V32() set
K6(K7(REAL,(REAL a))) is V2() V32() set
b is V11() real ext-real set
x0 is V11() real ext-real set
n is V11() real ext-real set
['x0,n'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
f is V11() real ext-real set
['b,f'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
F is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
F | ['b,f'] is Relation-like REAL -defined ['b,f'] -defined REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
dom F is V129() V130() V131() Element of K6(REAL)
F | ['x0,n'] is Relation-like REAL -defined ['x0,n'] -defined REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
c7 is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
proj (c7,a) is non empty Relation-like REAL a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL a),REAL))
K7((REAL a),REAL) is V2() Relation-like V32() complex-valued ext-real-valued real-valued set
K6(K7((REAL a),REAL)) is V2() V32() set
Seg a is V32() V39(a) V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT : ( 1 <= b1 & b1 <= a ) } is set
(proj (c7,a)) * F is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (c7,a)) * (F | ['b,f']) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((proj (c7,a)) * F) | ['b,f'] is Relation-like REAL -defined ['b,f'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (proj (c7,a)) is non empty functional FinSequence-membered V255() V256() V257() Element of K6((REAL a))
K6((REAL a)) is set
rng F is functional FinSequence-membered V255() V256() V257() Element of K6((REAL a))
dom ((proj (c7,a)) * F) is V129() V130() V131() Element of K6(REAL)
((proj (c7,a)) * F) | ['x0,n'] is Relation-like REAL -defined ['x0,n'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (c7,a)) * (F | ['x0,n']) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
c7 is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
proj (c7,a) is non empty Relation-like REAL a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL a),REAL))
(proj (c7,a)) * F is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
c7 is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
proj (c7,a) is non empty Relation-like REAL a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL a),REAL))
(proj (c7,a)) * (F | ['x0,n']) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
a is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
REAL a is non empty functional FinSequence-membered V255() V256() V257() FinSequenceSet of REAL
a -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = a } is set
K7(REAL,(REAL a)) is V2() Relation-like V32() set
K6(K7(REAL,(REAL a))) is V2() V32() set
b is V11() real ext-real set
x0 is V11() real ext-real set
n is V11() real ext-real set
['x0,n'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
f is V11() real ext-real set
['b,f'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
F is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
F | ['b,f'] is Relation-like REAL -defined ['b,f'] -defined REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
dom F is V129() V130() V131() Element of K6(REAL)
c7 is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
c7 | ['b,f'] is Relation-like REAL -defined ['b,f'] -defined REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
dom c7 is V129() V130() V131() Element of K6(REAL)
F + c7 is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
K771(REAL,REAL,(REAL a),(REAL a),F,c7) is Relation-like REAL /\ REAL -defined K703((K698((REAL a)) /\ K698((REAL a)))) -valued Function-like V261() V262() V263() Element of K6(K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a))))))
REAL /\ REAL is V129() V130() V131() V163() set
K698((REAL a)) is set
K698((REAL a)) /\ K698((REAL a)) is set
K703((K698((REAL a)) /\ K698((REAL a)))) is functional V255() V256() V257() set
K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a))))) is Relation-like set
K6(K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a)))))) is set
(F + c7) | ['x0,n'] is Relation-like REAL -defined ['x0,n'] -defined REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
x is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
proj (x,a) is non empty Relation-like REAL a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL a),REAL))
K7((REAL a),REAL) is V2() Relation-like V32() complex-valued ext-real-valued real-valued set
K6(K7((REAL a),REAL)) is V2() V32() set
Seg a is V32() V39(a) V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT : ( 1 <= b1 & b1 <= a ) } is set
(proj (x,a)) * F is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (x,a)) * (F | ['b,f']) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((proj (x,a)) * F) | ['b,f'] is Relation-like REAL -defined ['b,f'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (proj (x,a)) is non empty functional FinSequence-membered V255() V256() V257() Element of K6((REAL a))
K6((REAL a)) is set
rng F is functional FinSequence-membered V255() V256() V257() Element of K6((REAL a))
dom ((proj (x,a)) * F) is V129() V130() V131() Element of K6(REAL)
(proj (x,a)) * c7 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (x,a)) * (c7 | ['b,f']) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((proj (x,a)) * c7) | ['b,f'] is Relation-like REAL -defined ['b,f'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
rng c7 is functional FinSequence-membered V255() V256() V257() Element of K6((REAL a))
dom ((proj (x,a)) * c7) is V129() V130() V131() Element of K6(REAL)
((proj (x,a)) * F) + ((proj (x,a)) * c7) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(((proj (x,a)) * F) + ((proj (x,a)) * c7)) | ['x0,n'] is Relation-like REAL -defined ['x0,n'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (x,a)) * (F + c7) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((proj (x,a)) * (F + c7)) | ['x0,n'] is Relation-like REAL -defined ['x0,n'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (x,a)) * ((F + c7) | ['x0,n']) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
x is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
proj (x,a) is non empty Relation-like REAL a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL a),REAL))
(proj (x,a)) * (F + c7) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
x is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
proj (x,a) is non empty Relation-like REAL a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL a),REAL))
(proj (x,a)) * ((F + c7) | ['x0,n']) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
a is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
REAL a is non empty functional FinSequence-membered V255() V256() V257() FinSequenceSet of REAL
a -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = a } is set
K7(REAL,(REAL a)) is V2() Relation-like V32() set
K6(K7(REAL,(REAL a))) is V2() V32() set
b is V11() real ext-real set
x0 is V11() real ext-real set
n is V11() real ext-real set
['x0,n'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
f is V11() real ext-real set
['b,f'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
F is V11() real ext-real set
c7 is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
c7 | ['b,f'] is Relation-like REAL -defined ['b,f'] -defined REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
dom c7 is V129() V130() V131() Element of K6(REAL)
F (#) c7 is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
K740(REAL,(REAL a),c7,F) is Relation-like REAL -defined K703(K698((REAL a))) -valued Function-like V261() V262() V263() Element of K6(K7(REAL,K703(K698((REAL a)))))
K698((REAL a)) is set
K703(K698((REAL a))) is functional V255() V256() V257() set
K7(REAL,K703(K698((REAL a)))) is Relation-like set
K6(K7(REAL,K703(K698((REAL a))))) is set
(F (#) c7) | ['x0,n'] is Relation-like REAL -defined ['x0,n'] -defined REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
x is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
proj (x,a) is non empty Relation-like REAL a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL a),REAL))
K7((REAL a),REAL) is V2() Relation-like V32() complex-valued ext-real-valued real-valued set
K6(K7((REAL a),REAL)) is V2() V32() set
Seg a is V32() V39(a) V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT : ( 1 <= b1 & b1 <= a ) } is set
(proj (x,a)) * c7 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (x,a)) * (c7 | ['b,f']) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((proj (x,a)) * c7) | ['b,f'] is Relation-like REAL -defined ['b,f'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (proj (x,a)) is non empty functional FinSequence-membered V255() V256() V257() Element of K6((REAL a))
K6((REAL a)) is set
rng c7 is functional FinSequence-membered V255() V256() V257() Element of K6((REAL a))
dom ((proj (x,a)) * c7) is V129() V130() V131() Element of K6(REAL)
F (#) ((proj (x,a)) * c7) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(F (#) ((proj (x,a)) * c7)) | ['x0,n'] is Relation-like REAL -defined ['x0,n'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (x,a)) * (F (#) c7) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
((proj (x,a)) * (F (#) c7)) | ['x0,n'] is Relation-like REAL -defined ['x0,n'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(proj (x,a)) * ((F (#) c7) | ['x0,n']) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
x is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
proj (x,a) is non empty Relation-like REAL a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL a),REAL))
(proj (x,a)) * (F (#) c7) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
x is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
proj (x,a) is non empty Relation-like REAL a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL a),REAL))
(proj (x,a)) * ((F (#) c7) | ['x0,n']) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
a is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
REAL a is non empty functional FinSequence-membered V255() V256() V257() FinSequenceSet of REAL
a -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = a } is set
K7(REAL,(REAL a)) is V2() Relation-like V32() set
K6(K7(REAL,(REAL a))) is V2() V32() set
b is V11() real ext-real set
x0 is V11() real ext-real set
n is V11() real ext-real set
['x0,n'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
f is V11() real ext-real set
['b,f'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
F is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
F | ['b,f'] is Relation-like REAL -defined ['b,f'] -defined REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
dom F is V129() V130() V131() Element of K6(REAL)
- F is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
(- F) | ['x0,n'] is Relation-like REAL -defined ['x0,n'] -defined REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
- 1 is V11() real V44() V45() ext-real non positive Element of INT
(- 1) (#) F is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
K740(REAL,(REAL a),F,(- 1)) is Relation-like REAL -defined K703(K698((REAL a))) -valued Function-like V261() V262() V263() Element of K6(K7(REAL,K703(K698((REAL a)))))
K698((REAL a)) is set
K703(K698((REAL a))) is functional V255() V256() V257() set
K7(REAL,K703(K698((REAL a)))) is Relation-like set
K6(K7(REAL,K703(K698((REAL a))))) is set
a is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
REAL a is non empty functional FinSequence-membered V255() V256() V257() FinSequenceSet of REAL
a -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = a } is set
K7(REAL,(REAL a)) is V2() Relation-like V32() set
K6(K7(REAL,(REAL a))) is V2() V32() set
b is V11() real ext-real set
x0 is V11() real ext-real set
n is V11() real ext-real set
['x0,n'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
f is V11() real ext-real set
['b,f'] is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
F is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
F | ['b,f'] is Relation-like REAL -defined ['b,f'] -defined REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
dom F is V129() V130() V131() Element of K6(REAL)
c7 is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
c7 | ['b,f'] is Relation-like REAL -defined ['b,f'] -defined REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
dom c7 is V129() V130() V131() Element of K6(REAL)
F - c7 is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
K777(REAL,REAL,(REAL a),(REAL a),F,c7) is Relation-like REAL /\ REAL -defined K703((K698((REAL a)) /\ K698((REAL a)))) -valued Function-like V261() V262() V263() Element of K6(K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a))))))
REAL /\ REAL is V129() V130() V131() V163() set
K698((REAL a)) is set
K698((REAL a)) /\ K698((REAL a)) is set
K703((K698((REAL a)) /\ K698((REAL a)))) is functional V255() V256() V257() set
K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a))))) is Relation-like set
K6(K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a)))))) is set
(F - c7) | ['x0,n'] is Relation-like REAL -defined ['x0,n'] -defined REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
- c7 is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
dom (- c7) is V129() V130() V131() Element of K6(REAL)
F + (- c7) is Relation-like REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
K771(REAL,REAL,(REAL a),(REAL a),F,(- c7)) is Relation-like REAL /\ REAL -defined K703((K698((REAL a)) /\ K698((REAL a)))) -valued Function-like V261() V262() V263() Element of K6(K7((REAL /\ REAL),K703((K698((REAL a)) /\ K698((REAL a))))))
(- c7) | ['b,f'] is Relation-like REAL -defined ['b,f'] -defined REAL -defined REAL a -valued Function-like V261() V262() V263() Element of K6(K7(REAL,(REAL a)))
a is non empty V129() V130() V131() V160() V161() V162() V163() closed_interval compact closed Element of K6(REAL)
b is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real positive non negative V129() V130() V131() V132() V133() V134() V158() V159() V160() V161() V162() Element of NAT
REAL b is non empty functional FinSequence-membered V255() V256() V257() FinSequenceSet of REAL
b -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like Element of REAL * : len b1 = b } is set
K7(a,(REAL b)) is Relation-like set
K6(K7(a,(REAL b))) is set
x0 is non empty Relation-like a -defined REAL b -valued Function-like total quasi_total V261() V262() V263() Element of K6(K7(a,(REAL b)))
|.x0.| is Relation-like a -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
K7(a,REAL) is V2() Relation-like V32() complex-valued ext-real-valued real-valued set
K6(K7(a,REAL)) is V2() V32() set
Seg b is non empty V32() V39(b) V129() V130() V131() V132() V133() V134() V158() V159() V160() V161() V162() Element of K6(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT : ( 1 <= b1 & b1 <= b ) } is set
n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() ext-real non negative set
proj (n,b) is non empty Relation-like REAL b -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL b),REAL))
K7((REAL b),REAL) is V2() Relation-like V32() complex-valued ext-real-valued real-valued set
K6(K7((REAL b),REAL)) is V2() V32() set
(proj (n,b)) * x0 is non empty Relation-like a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
dom ((proj (n,b)) * x0) is non empty V129() V130() V131() Element of K6(a)
K6(a) is set
F is V11() real ext-real set
c7 is set
abs F is V11() real ext-real Element of REAL
((proj (n,b)) * x0) . c7 is V11() real ext-real Element of REAL
abs (((proj (n,b)) * x0) . c7) is V11() real ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
dom n is V32() V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of K6(NAT)
f is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
proj (f,b) is non empty Relation-like REAL b -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL b),REAL))
K7((REAL b),REAL) is V2() Relation-like V32() complex-valued ext-real-valued real-valued set
K6(K7((REAL b),REAL)) is V2() V32() set
n . f is V11() real ext-real Element of REAL
(proj (f,b)) * x0 is non empty Relation-like a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
dom ((proj (f,b)) * x0) is non empty V129() V130() V131() Element of K6(a)
K6(a) is set
c7 is set
((proj (f,b)) * x0) . c7 is V11() real ext-real Element of REAL
abs (((proj (f,b)) * x0) . c7) is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
len n is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like V32() V39(b) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL b
F is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
f . F is V11() real ext-real Element of REAL
Sum f is V11() real ext-real Element of REAL
dom |.x0.| is V129() V130() V131() Element of K6(a)
b * (Sum f) is V11() real ext-real Element of REAL
(b * (Sum f)) + 1 is V11() real ext-real Element of REAL
c7 is set
|.x0.| . c7 is V11() real ext-real Element of REAL
abs (|.x0.| . c7) is V11() real ext-real Element of REAL
|.x0.| /. c7 is V11() real ext-real Element of REAL
x0 /. c7 is Relation-like NAT -defined Function-like V32() V39(b) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL b
|.(x0 /. c7).| is V11() real ext-real non negative Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real V32() V37() V44() V45() ext-real non negative V129() V130() V131() V132() V133() V134() V160() V161() V162() Element of NAT
proj (x,b) is non empty Relation-like REAL b -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((REAL b),REAL))
dom x0 is non empty V129() V130() V131() Element of K6(a)
x0 . c7 is Relation-like NAT -defined Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
rng x0 is non empty functional FinSequence-membered V255() V256() V257() Element of K6((REAL b))
K6((REAL b)) is set
dom (proj (x,b)) is non empty functional FinSequence-membered V255() V256() V257() Element of K6((REAL b))
(proj (x,b)) * x0 is non empty Relation-like a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
dom ((proj (x,b)) * x0) is non empty V129() V130() V131() Element of K6(a)
f . x is V11() real ext-real Element of REAL
((proj (x,b)) * x0) . c7 is V11() real ext-real Element of REAL
abs (((proj (x,b)) * x0) . c7) is V11() real ext-real Element of REAL
(proj (x,b)) . (x0 . c7) is V11() real ext-real Element of REAL
abs ((proj (x,b)) . (x0 . c7)) is V11() real ext-real Element of REAL
(proj (x,b)) . (