:: INTEGRA6 semantic presentation

REAL is non empty V2() V45() V46() V47() V51() V58() non bounded_below non bounded_above interval set
NAT is non empty V2() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V58() V63() V64() left_end bounded_below Element of K6(REAL)
K6(REAL) is V2() V58() set
COMPLEX is non empty V2() V45() V51() V58() set
RAT is non empty V2() V45() V46() V47() V48() V51() V58() set
INT is non empty V2() V45() V46() V47() V48() V49() V51() V58() set
K7(COMPLEX,COMPLEX) is V2() Relation-like complex-valued V58() set
K6(K7(COMPLEX,COMPLEX)) is V2() V58() set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V2() Relation-like complex-valued V58() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is V2() V58() set
K7(REAL,REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(REAL,REAL)) is V2() V58() set
K7(K7(REAL,REAL),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(K7(REAL,REAL),REAL)) is V2() V58() set
K7(RAT,RAT) is V2() Relation-like RAT -valued complex-valued ext-real-valued real-valued V58() set
K6(K7(RAT,RAT)) is V2() V58() set
K7(K7(RAT,RAT),RAT) is V2() Relation-like RAT -valued complex-valued ext-real-valued real-valued V58() set
K6(K7(K7(RAT,RAT),RAT)) is V2() V58() set
K7(INT,INT) is V2() Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued V58() set
K6(K7(INT,INT)) is V2() V58() set
K7(K7(INT,INT),INT) is V2() Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued V58() set
K6(K7(K7(INT,INT),INT)) is V2() V58() set
K7(NAT,NAT) is V2() Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued V58() set
K7(K7(NAT,NAT),NAT) is V2() Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued V58() set
K6(K7(K7(NAT,NAT),NAT)) is V2() V58() set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued functional integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V46() V47() V48() V49() V50() V51() V58() V59() V62() V63() V65( {} ) FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
{{},1} is non empty V45() V46() V47() V48() V49() V50() V58() V62() left_end right_end bounded_below bounded_above real-bounded set
omega is non empty V2() epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V58() V63() V64() left_end bounded_below set
K6(omega) is V2() V58() set
K6(NAT) is V2() V58() set
K7(NAT,REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(NAT,REAL)) is V2() V58() 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 V58() set
K7(K7(REAL,the_set_of_RealSequences),the_set_of_RealSequences) is V2() Relation-like V58() set
K6(K7(K7(REAL,the_set_of_RealSequences),the_set_of_RealSequences)) is V2() V58() set
Linear_Space_of_RealSequences is L12()
the U1 of Linear_Space_of_RealSequences is set
K6( the U1 of Linear_Space_of_RealSequences) is set
the_set_of_l2RealSequences is Element of K6( the U1 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
ExtREAL is non empty V46() interval set
K7(COMPLEX,REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(COMPLEX,REAL)) is V2() V58() set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued functional integer V31() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V46() V47() V48() V49() V50() V51() V58() V59() V62() V63() V65( {} ) FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
a is V11() real ext-real set
b is V11() real ext-real set
f is V11() real ext-real set
a + f is V11() real ext-real set
x0 is V11() real ext-real set
b + x0 is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
f is V11() real ext-real set
f - a is V11() real ext-real set
- a is V11() real ext-real set
f + (- a) is V11() real ext-real set
f + a is V11() real ext-real set
].(f - a),(f + a).[ is V45() V46() V47() open non left_end non right_end interval Element of K6(REAL)
f - b is V11() real ext-real set
- b is V11() real ext-real set
f + (- b) is V11() real ext-real set
f + b is V11() real ext-real set
].(f - b),(f + b).[ is V45() V46() V47() open non left_end non right_end interval Element of K6(REAL)
a is Relation-like set
b is set
f is set
x0 is set
a | f is Relation-like set
(a | f) | b is Relation-like set
a | x0 is Relation-like set
(a | x0) | b is Relation-like set
a | b is Relation-like set
a is set
b is set
f is set
chi (b,b) is Relation-like b -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(b,REAL))
K7(b,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(b,REAL)) is set
(chi (b,b)) | a is Relation-like a -defined b -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(b,REAL))
chi (f,f) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(f,REAL))
K7(f,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7(f,REAL)) is set
(chi (f,f)) | a is Relation-like a -defined f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(f,REAL))
dom ((chi (f,f)) | a) is set
dom (chi (f,f)) is set
(dom (chi (f,f))) /\ a is set
f /\ a is set
dom ((chi (b,b)) | a) is set
dom (chi (b,b)) is set
(dom (chi (b,b))) /\ a is set
b /\ a is set
x0 is set
((chi (b,b)) | a) . x0 is V11() real ext-real Element of REAL
(chi (b,b)) . x0 is V11() real ext-real Element of REAL
(chi (f,f)) . x0 is V11() real ext-real Element of REAL
((chi (f,f)) | a) . x0 is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
vol ['a,b'] is V11() real ext-real Element of REAL
upper_bound ['a,b'] is V11() real ext-real Element of REAL
lower_bound ['a,b'] is V11() real ext-real Element of REAL
(upper_bound ['a,b']) - (lower_bound ['a,b']) is V11() real ext-real Element of REAL
- (lower_bound ['a,b']) is V11() real ext-real set
(upper_bound ['a,b']) + (- (lower_bound ['a,b'])) is V11() real ext-real set
b - a is V11() real ext-real set
- a is V11() real ext-real set
b + (- a) is V11() real ext-real set
[.a,b.] is V45() V46() V47() closed interval Element of K6(REAL)
lower_bound [.a,b.] is V11() real ext-real Element of REAL
upper_bound [.a,b.] is V11() real ext-real Element of REAL
[.(lower_bound [.a,b.]),(upper_bound [.a,b.]).] is V45() V46() V47() closed interval Element of K6(REAL)
a is V11() real ext-real set
b is V11() real ext-real set
min (a,b) is V11() real ext-real set
max (a,b) is V11() real ext-real set
['(min (a,b)),(max (a,b))'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
vol ['(min (a,b)),(max (a,b))'] is V11() real ext-real Element of REAL
upper_bound ['(min (a,b)),(max (a,b))'] is V11() real ext-real Element of REAL
lower_bound ['(min (a,b)),(max (a,b))'] is V11() real ext-real Element of REAL
(upper_bound ['(min (a,b)),(max (a,b))']) - (lower_bound ['(min (a,b)),(max (a,b))']) is V11() real ext-real Element of REAL
- (lower_bound ['(min (a,b)),(max (a,b))']) is V11() real ext-real set
(upper_bound ['(min (a,b)),(max (a,b))']) + (- (lower_bound ['(min (a,b)),(max (a,b))'])) is V11() real ext-real set
b - a is V11() real ext-real set
- a is V11() real ext-real set
b + (- a) is V11() real ext-real set
abs (b - a) is V11() real ext-real Element of REAL
a - b is V11() real ext-real set
- b is V11() real ext-real set
a + (- b) is V11() real ext-real set
abs (a - b) is V11() real ext-real Element of REAL
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
K7(a,REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(a,REAL)) is V2() V58() set
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 set
b || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
rng b is V45() V46() V47() Element of K6(REAL)
K7((dom b),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7((dom b),REAL)) is set
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval 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 set
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))
abs b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral (b,a) is V11() real ext-real Element of REAL
b || a is Relation-like a -defined REAL -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 complex-valued ext-real-valued real-valued V58() set
K6(K7(a,REAL)) is V2() V58() set
integral (b || a) is V11() real ext-real Element of REAL
upper_integral (b || a) is V11() real ext-real Element of REAL
upper_sum_set (b || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
divs a is non empty set
K7((divs a),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs a),REAL)) is V2() V58() set
rng (upper_sum_set (b || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (b || a))) is V11() real ext-real Element of REAL
abs (integral (b,a)) is V11() real ext-real Element of REAL
integral ((abs b),a) is V11() real ext-real Element of REAL
(abs b) || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
integral ((abs b) || a) is V11() real ext-real Element of REAL
upper_integral ((abs b) || a) is V11() real ext-real Element of REAL
upper_sum_set ((abs b) || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
rng (upper_sum_set ((abs b) || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((abs b) || a))) is V11() real ext-real Element of REAL
abs (b || a) is Relation-like REAL -defined a -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(b || a) | a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval 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))
dom f is set
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))
integral (f,a,b) is V11() real ext-real Element of REAL
abs (integral (f,a,b)) 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 Element of K6(K7(REAL,REAL))
integral ((abs f),a,b) is V11() real ext-real Element of REAL
integral (f,['a,b']) is V11() real ext-real Element of REAL
f || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
K7(['a,b'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['a,b'],REAL)) is V2() V58() set
integral (f || ['a,b']) is V11() real ext-real Element of REAL
upper_integral (f || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set (f || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
divs ['a,b'] is non empty set
K7((divs ['a,b']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['a,b']),REAL)) is V2() V58() set
rng (upper_sum_set (f || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (f || ['a,b']))) is V11() real ext-real Element of REAL
integral ((abs f),['a,b']) is V11() real ext-real Element of REAL
(abs f) || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
integral ((abs f) || ['a,b']) is V11() real ext-real Element of REAL
upper_integral ((abs f) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set ((abs f) || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set ((abs f) || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((abs f) || ['a,b']))) is V11() real ext-real Element of REAL
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval 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 set
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))
integral (b,a) is V11() real ext-real Element of REAL
b || a is Relation-like a -defined REAL -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 complex-valued ext-real-valued real-valued V58() set
K6(K7(a,REAL)) is V2() V58() set
integral (b || a) is V11() real ext-real Element of REAL
upper_integral (b || a) is V11() real ext-real Element of REAL
upper_sum_set (b || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
divs a is non empty set
K7((divs a),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs a),REAL)) is V2() V58() set
rng (upper_sum_set (b || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (b || a))) is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
f (#) b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((f (#) b),a) is V11() real ext-real Element of REAL
(f (#) b) || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
integral ((f (#) b) || a) is V11() real ext-real Element of REAL
upper_integral ((f (#) b) || a) is V11() real ext-real Element of REAL
upper_sum_set ((f (#) b) || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
rng (upper_sum_set ((f (#) b) || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((f (#) b) || a))) is V11() real ext-real Element of REAL
f * (integral (b,a)) is V11() real ext-real Element of REAL
(b || a) | a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
rng b is V45() V46() V47() Element of K6(REAL)
K7((dom b),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7((dom b),REAL)) is set
f (#) (b || a) is Relation-like REAL -defined a -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(f (#) 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))
integral (f (#) (b || a)) is V11() real ext-real Element of REAL
upper_integral (f (#) (b || a)) is V11() real ext-real Element of REAL
upper_sum_set (f (#) (b || a)) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
rng (upper_sum_set (f (#) (b || a))) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (f (#) (b || a)))) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is V11() real ext-real set
x0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom x0 is set
x0 | ['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))
f (#) x0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((f (#) x0),a,b) is V11() real ext-real Element of REAL
integral (x0,a,b) is V11() real ext-real Element of REAL
f * (integral (x0,a,b)) is V11() real ext-real Element of REAL
integral (x0,['a,b']) is V11() real ext-real Element of REAL
x0 || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
K7(['a,b'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['a,b'],REAL)) is V2() V58() set
integral (x0 || ['a,b']) is V11() real ext-real Element of REAL
upper_integral (x0 || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set (x0 || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
divs ['a,b'] is non empty set
K7((divs ['a,b']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['a,b']),REAL)) is V2() V58() set
rng (upper_sum_set (x0 || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (x0 || ['a,b']))) is V11() real ext-real Element of REAL
integral ((f (#) x0),['a,b']) is V11() real ext-real Element of REAL
(f (#) x0) || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
integral ((f (#) x0) || ['a,b']) is V11() real ext-real Element of REAL
upper_integral ((f (#) x0) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set ((f (#) x0) || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set ((f (#) x0) || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((f (#) x0) || ['a,b']))) is V11() real ext-real Element of REAL
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval 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 set
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))
integral (b,a) is V11() real ext-real Element of REAL
b || a is Relation-like a -defined REAL -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 complex-valued ext-real-valued real-valued V58() set
K6(K7(a,REAL)) is V2() V58() set
integral (b || a) is V11() real ext-real Element of REAL
upper_integral (b || a) is V11() real ext-real Element of REAL
upper_sum_set (b || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
divs a is non empty set
K7((divs a),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs a),REAL)) is V2() V58() set
rng (upper_sum_set (b || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (b || a))) 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))
dom f is set
f | 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))
b + f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
b - f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((b + f),a) is V11() real ext-real Element of REAL
(b + f) || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
integral ((b + f) || a) is V11() real ext-real Element of REAL
upper_integral ((b + f) || a) is V11() real ext-real Element of REAL
upper_sum_set ((b + f) || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
rng (upper_sum_set ((b + f) || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((b + f) || a))) is V11() real ext-real Element of REAL
integral (f,a) is V11() real ext-real Element of REAL
f || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
integral (f || a) is V11() real ext-real Element of REAL
upper_integral (f || a) is V11() real ext-real Element of REAL
upper_sum_set (f || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
rng (upper_sum_set (f || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (f || a))) is V11() real ext-real Element of REAL
(integral (b,a)) + (integral (f,a)) is V11() real ext-real Element of REAL
integral ((b - f),a) is V11() real ext-real Element of REAL
(b - f) || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
integral ((b - f) || a) is V11() real ext-real Element of REAL
upper_integral ((b - f) || a) is V11() real ext-real Element of REAL
upper_sum_set ((b - f) || a) is non empty Relation-like divs a -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs a),REAL))
rng (upper_sum_set ((b - f) || a)) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((b - f) || a))) is V11() real ext-real Element of REAL
(integral (b,a)) - (integral (f,a)) is V11() real ext-real Element of REAL
- (integral (f,a)) is V11() real ext-real set
(integral (b,a)) + (- (integral (f,a))) is V11() real ext-real set
(b || a) | a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(f || a) | a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(b || a) + (f || a) is Relation-like REAL -defined a -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(b || a) - (f || a) is Relation-like REAL -defined a -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval 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))
dom f is set
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))
integral (f,a,b) is V11() real ext-real Element of REAL
x0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom x0 is set
x0 | ['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))
f + x0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((f + x0),a,b) is V11() real ext-real Element of REAL
integral (x0,a,b) is V11() real ext-real Element of REAL
(integral (f,a,b)) + (integral (x0,a,b)) is V11() real ext-real Element of REAL
f - x0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((f - x0),a,b) is V11() real ext-real Element of REAL
(integral (f,a,b)) - (integral (x0,a,b)) is V11() real ext-real Element of REAL
- (integral (x0,a,b)) is V11() real ext-real set
(integral (f,a,b)) + (- (integral (x0,a,b))) is V11() real ext-real set
integral ((f + x0),['a,b']) is V11() real ext-real Element of REAL
(f + x0) || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
K7(['a,b'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['a,b'],REAL)) is V2() V58() set
integral ((f + x0) || ['a,b']) is V11() real ext-real Element of REAL
upper_integral ((f + x0) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set ((f + x0) || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
divs ['a,b'] is non empty set
K7((divs ['a,b']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['a,b']),REAL)) is V2() V58() set
rng (upper_sum_set ((f + x0) || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((f + x0) || ['a,b']))) is V11() real ext-real Element of REAL
integral ((f - x0),['a,b']) is V11() real ext-real Element of REAL
(f - x0) || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
integral ((f - x0) || ['a,b']) is V11() real ext-real Element of REAL
upper_integral ((f - x0) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set ((f - x0) || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set ((f - x0) || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((f - x0) || ['a,b']))) is V11() real ext-real Element of REAL
integral (f,['a,b']) is V11() real ext-real Element of REAL
f || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
integral (f || ['a,b']) is V11() real ext-real Element of REAL
upper_integral (f || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set (f || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set (f || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (f || ['a,b']))) is V11() real ext-real Element of REAL
integral (x0,['a,b']) is V11() real ext-real Element of REAL
x0 || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
integral (x0 || ['a,b']) is V11() real ext-real Element of REAL
upper_integral (x0 || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set (x0 || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set (x0 || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (x0 || ['a,b']))) is V11() real ext-real Element of REAL
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval 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))
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))
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 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))
b (#) f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(b (#) f) | 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))
a /\ a is V45() V46() V47() interval Element of K6(REAL)
(b (#) f) | (a /\ a) is Relation-like REAL -defined a /\ a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval 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 set
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))
f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom f is set
f | 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))
b (#) f is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
b || a is Relation-like a -defined REAL -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 complex-valued ext-real-valued real-valued V58() set
K6(K7(a,REAL)) is V2() V58() set
(b || a) | a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
f || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(f || a) | a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(b || a) (#) (f || a) is Relation-like REAL -defined a -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
(b (#) f) || a is Relation-like a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(a,REAL))
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
vol a is V11() real ext-real Element of REAL
upper_bound a is V11() real ext-real Element of REAL
lower_bound a is V11() real ext-real Element of REAL
(upper_bound a) - (lower_bound a) is V11() real ext-real Element of REAL
- (lower_bound a) is V11() real ext-real set
(upper_bound a) + (- (lower_bound a)) is V11() real ext-real set
b is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(vol a) / b is V11() real ext-real Element of REAL
b " is V11() real ext-real non negative set
(vol a) * (b ") is V11() real ext-real set
f is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
len f is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
dom f is V45() V46() V47() V48() V49() V50() V58() bounded_below bounded_above real-bounded Element of K6(NAT)
x0 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
f . F is V11() real ext-real Element of REAL
f . x0 is V11() real ext-real Element of REAL
((vol a) / b) * F is V11() real ext-real Element of REAL
((vol a) / b) * x0 is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / b) * F) is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / b) * x0) is V11() real ext-real Element of REAL
Seg b is V45() V46() V47() V48() V49() V50() V58() V65(b) bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= b ) } is set
x0 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like FinSequence of REAL
len x0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
x0 . (len x0) is V11() real ext-real Element of REAL
((vol a) / b) * b is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / b) * b) is V11() real ext-real Element of REAL
(lower_bound a) + (vol a) is V11() real ext-real Element of REAL
rng x0 is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
F is set
dom x0 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
c₆ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
x0 . c₆ is V11() real ext-real Element of REAL
((vol a) / b) * c₆ is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / b) * c₆) is V11() real ext-real Element of REAL
F is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
len F is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom F is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
c₆ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
F . c₆ is V11() real ext-real Element of REAL
((vol a) / b) * c₆ is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / b) * c₆) is V11() real ext-real Element of REAL
a is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
vol a is V11() real ext-real Element of REAL
upper_bound a is V11() real ext-real Element of REAL
lower_bound a is V11() real ext-real Element of REAL
(upper_bound a) - (lower_bound a) is V11() real ext-real Element of REAL
- (lower_bound a) is V11() real ext-real set
(upper_bound a) + (- (lower_bound a)) is V11() real ext-real set
divs a is non empty set
K7(NAT,(divs a)) is V2() Relation-like V58() set
K6(K7(NAT,(divs a))) is V2() V58() set
b is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(vol a) / (b + 1) is V11() real ext-real Element of REAL
(b + 1) " is non empty V11() real ext-real positive non negative set
(vol a) * ((b + 1) ") is V11() real ext-real set
f is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
len f is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom f is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
x0 is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like Element of divs a
b is non empty Relation-like NAT -defined divs a -valued Function-like total quasi_total Element of K6(K7(NAT,(divs a)))
f is non empty Relation-like NAT -defined divs a -valued Function-like total quasi_total Element of K6(K7(NAT,(divs a)))
x0 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
x0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
f . x0 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
F is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
c₆ is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
F + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
delta f 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))
x0 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(delta f) . x0 is V11() real ext-real Element of REAL
x0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(vol a) / (x0 + 1) is V11() real ext-real Element of REAL
(x0 + 1) " is non empty V11() real ext-real positive non negative set
(vol a) * ((x0 + 1) ") is V11() real ext-real set
chi (a,a) 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 complex-valued ext-real-valued real-valued V58() set
K6(K7(a,REAL)) is V2() V58() set
f . x0 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
upper_volume ((chi (a,a)),(f . x0)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (upper_volume ((chi (a,a)),(f . x0))) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
{((vol a) / (x0 + 1))} is non empty V2() V45() V46() V47() V58() V65(1) left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
c₆ is set
dom (upper_volume ((chi (a,a)),(f . x0))) is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
x is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(upper_volume ((chi (a,a)),(f . x0))) . x is V11() real ext-real Element of REAL
len (upper_volume ((chi (a,a)),(f . x0))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len (upper_volume ((chi (a,a)),(f . x0)))) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len (upper_volume ((chi (a,a)),(f . x0)))) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len (upper_volume ((chi (a,a)),(f . x0))) ) } is set
F is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
len F is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len F) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len F) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len F ) } is set
dom F is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
divset (F,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
upper_bound (divset (F,x)) is V11() real ext-real Element of REAL
lower_bound (divset (F,x)) is V11() real ext-real Element of REAL
(upper_bound (divset (F,x))) - (lower_bound (divset (F,x))) is V11() real ext-real Element of REAL
- (lower_bound (divset (F,x))) is V11() real ext-real set
(upper_bound (divset (F,x))) + (- (lower_bound (divset (F,x)))) is V11() real ext-real set
L is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
L + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
F . 1 is V11() real ext-real Element of REAL
((vol a) / (x0 + 1)) * 1 is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / (x0 + 1)) * 1) is V11() real ext-real Element of REAL
L is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
L + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(lower_bound a) + ((vol a) / (x0 + 1)) is V11() real ext-real Element of REAL
((lower_bound a) + ((vol a) / (x0 + 1))) - (lower_bound a) is V11() real ext-real Element of REAL
((lower_bound a) + ((vol a) / (x0 + 1))) + (- (lower_bound a)) is V11() real ext-real set
x - 1 is V11() real integer ext-real Element of REAL
- 1 is V11() real integer ext-real non positive set
x + (- 1) is V11() real integer ext-real set
F . (x - 1) is V11() real ext-real Element of REAL
(vol a) / (len F) is V11() real ext-real Element of REAL
(len F) " is non empty V11() real ext-real positive non negative set
(vol a) * ((len F) ") is V11() real ext-real set
((vol a) / (len F)) * (x - 1) is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / (len F)) * (x - 1)) is V11() real ext-real Element of REAL
L is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
L + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
F . x is V11() real ext-real Element of REAL
((vol a) / (len F)) * x is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / (len F)) * x) is V11() real ext-real Element of REAL
L is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
L + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
L is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
L + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
vol (divset (F,x)) is V11() real ext-real Element of REAL
c₆ is set
F is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
rng F is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
dom F is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
divset (F,1) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
upper_bound (divset (F,1)) is V11() real ext-real Element of REAL
F . 1 is V11() real ext-real Element of REAL
len F is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(vol a) / (len F) is V11() real ext-real Element of REAL
(len F) " is non empty V11() real ext-real positive non negative set
(vol a) * ((len F) ") is V11() real ext-real set
((vol a) / (len F)) * 1 is V11() real ext-real Element of REAL
(lower_bound a) + (((vol a) / (len F)) * 1) is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
L is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
vol (divset (F,1)) is V11() real ext-real Element of REAL
lower_bound (divset (F,1)) is V11() real ext-real Element of REAL
(upper_bound (divset (F,1))) - (lower_bound (divset (F,1))) is V11() real ext-real Element of REAL
- (lower_bound (divset (F,1))) is V11() real ext-real set
(upper_bound (divset (F,1))) + (- (lower_bound (divset (F,1)))) is V11() real ext-real set
(lower_bound a) + ((vol a) / (len F)) is V11() real ext-real Element of REAL
((lower_bound a) + ((vol a) / (len F))) - (lower_bound a) is V11() real ext-real Element of REAL
((lower_bound a) + ((vol a) / (len F))) + (- (lower_bound a)) is V11() real ext-real set
Seg (len F) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len F) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len F ) } is set
upper_volume ((chi (a,a)),F) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
len (upper_volume ((chi (a,a)),F)) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len (upper_volume ((chi (a,a)),F))) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len (upper_volume ((chi (a,a)),F))) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len (upper_volume ((chi (a,a)),F)) ) } is set
dom (upper_volume ((chi (a,a)),F)) is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
(upper_volume ((chi (a,a)),F)) . 1 is V11() real ext-real Element of REAL
rng (upper_volume ((chi (a,a)),F)) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
x is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
L is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
delta (f . x0) is V11() real ext-real Element of REAL
sup (rng (upper_volume ((chi (a,a)),(f . x0)))) is V11() real ext-real set
x0 is V11() real ext-real Element of REAL
(vol a) / x0 is V11() real ext-real Element of REAL
x0 " is V11() real ext-real set
(vol a) * (x0 ") is V11() real ext-real set
[\((vol a) / x0)/] is V11() real integer ext-real set
[\((vol a) / x0)/] + 1 is V11() real integer ext-real Element of REAL
F is V11() real integer ext-real set
c₆ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
c₆ + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
1 * (c₆ + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
1 * x0 is V11() real ext-real Element of REAL
(vol a) / (c₆ + 1) is V11() real ext-real Element of REAL
(c₆ + 1) " is non empty V11() real ext-real positive non negative set
(vol a) * ((c₆ + 1) ") is V11() real ext-real set
(delta f) . c₆ is V11() real ext-real Element of REAL
((vol a) / (c₆ + 1)) - 0 is V11() real ext-real Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued functional integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V46() V47() V48() V49() V50() V51() V58() V59() V62() V63() V65( {} ) FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval set
((vol a) / (c₆ + 1)) + (- 0) is V11() real ext-real set
abs (((vol a) / (c₆ + 1)) - 0) is V11() real ext-real Element of REAL
x0 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
F is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(delta f) . F is V11() real ext-real Element of REAL
(delta f) . x0 is V11() real ext-real Element of REAL
x0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
F + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(vol a) / (F + 1) is V11() real ext-real Element of REAL
(F + 1) " is non empty V11() real ext-real positive non negative set
(vol a) * ((F + 1) ") is V11() real ext-real set
(vol a) / (x0 + 1) is V11() real ext-real Element of REAL
(x0 + 1) " is non empty V11() real ext-real positive non negative set
(vol a) * ((x0 + 1) ") is V11() real ext-real set
x0 is V11() real ext-real set
F is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(delta f) . F is V11() real ext-real Element of REAL
((delta f) . F) - 0 is V11() real ext-real Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued functional integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V46() V47() V48() V49() V50() V51() V58() V59() V62() V63() V65( {} ) FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval set
((delta f) . F) + (- 0) is V11() real ext-real set
abs (((delta f) . F) - 0) is V11() real ext-real Element of REAL
f . F is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
delta (f . F) is V11() real ext-real Element of REAL
chi (a,a) 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 complex-valued ext-real-valued real-valued V58() set
K6(K7(a,REAL)) is V2() V58() set
upper_volume ((chi (a,a)),(f . F)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (upper_volume ((chi (a,a)),(f . F))) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
sup (rng (upper_volume ((chi (a,a)),(f . F)))) is V11() real ext-real set
c₆ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(delta f) . c₆ is V11() real ext-real Element of REAL
f . c₆ is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of a
delta (f . c₆) is V11() real ext-real Element of REAL
upper_volume ((chi (a,a)),(f . c₆)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (upper_volume ((chi (a,a)),(f . c₆))) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
sup (rng (upper_volume ((chi (a,a)),(f . c₆)))) is V11() real ext-real set
((delta f) . c₆) - 0 is V11() real ext-real Element of REAL
((delta f) . c₆) + (- 0) is V11() real ext-real set
abs (((delta f) . c₆) - 0) is V11() real ext-real Element of REAL
lim (delta f) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is V11() real ext-real set
['a,f'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
['f,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
x0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom x0 is set
x0 | ['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))
integral (x0,a,b) is V11() real ext-real Element of REAL
integral (x0,a,f) is V11() real ext-real Element of REAL
integral (x0,f,b) is V11() real ext-real Element of REAL
(integral (x0,a,f)) + (integral (x0,f,b)) is V11() real ext-real Element of REAL
[.a,b.] is V45() V46() V47() closed interval Element of K6(REAL)
[.f,b.] is V45() V46() V47() closed interval Element of K6(REAL)
lower_bound [.f,b.] is V11() real ext-real Element of REAL
upper_bound [.f,b.] is V11() real ext-real Element of REAL
[.(lower_bound [.f,b.]),(upper_bound [.f,b.]).] is V45() V46() V47() closed interval Element of K6(REAL)
upper_bound ['f,b'] is V11() real ext-real Element of REAL
x0 || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
K7(['a,b'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['a,b'],REAL)) is V2() V58() set
x0 || ['a,f'] is Relation-like ['a,f'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,f'],REAL))
K7(['a,f'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['a,f'],REAL)) is V2() V58() set
x0 || ['f,b'] is Relation-like ['f,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['f,b'],REAL))
K7(['f,b'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['f,b'],REAL)) is V2() V58() set
[.a,f.] is V45() V46() V47() closed interval Element of K6(REAL)
lower_bound [.a,f.] is V11() real ext-real Element of REAL
upper_bound [.a,f.] is V11() real ext-real Element of REAL
[.(lower_bound [.a,f.]),(upper_bound [.a,f.]).] is V45() V46() V47() closed interval Element of K6(REAL)
lower_bound ['a,f'] is V11() real ext-real Element of REAL
x0 | ['f,b'] is Relation-like REAL -defined ['f,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(x0 || ['f,b']) | ['f,b'] is Relation-like ['f,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['f,b'],REAL))
lower_bound ['f,b'] is V11() real ext-real Element of REAL
divs ['f,b'] is non empty set
K7(NAT,(divs ['f,b'])) is V2() Relation-like V58() set
K6(K7(NAT,(divs ['f,b']))) is V2() V58() set
vol ['f,b'] is V11() real ext-real Element of REAL
(upper_bound ['f,b']) - (lower_bound ['f,b']) is V11() real ext-real Element of REAL
- (lower_bound ['f,b']) is V11() real ext-real set
(upper_bound ['f,b']) + (- (lower_bound ['f,b'])) is V11() real ext-real set
L is non empty Relation-like NAT -defined divs ['f,b'] -valued Function-like total quasi_total Element of K6(K7(NAT,(divs ['f,b'])))
delta L 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))
lim (delta L) is V11() real ext-real Element of REAL
R is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
L . R is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
R is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
N is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
R is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
len R is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
L is non empty Relation-like NAT -defined divs ['f,b'] -valued Function-like total quasi_total Element of K6(K7(NAT,(divs ['f,b'])))
delta L 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))
lim (delta L) is V11() real ext-real Element of REAL
R is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
L is non empty Relation-like NAT -defined divs ['f,b'] -valued Function-like total quasi_total Element of K6(K7(NAT,(divs ['f,b'])))
delta L 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))
lim (delta L) is V11() real ext-real Element of REAL
R is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R + R is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
L . (R + R) is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
N is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like Element of divs ['f,b']
R is non empty Relation-like NAT -defined divs ['f,b'] -valued Function-like total quasi_total Element of K6(K7(NAT,(divs ['f,b'])))
N is non empty Relation-like NAT -defined divs ['f,b'] -valued Function-like total quasi_total Element of K6(K7(NAT,(divs ['f,b'])))
R is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
N . R is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
x is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
e is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
x + R is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
L . (x + R) is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
R is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
N . R is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
x is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
x /^ 1 is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
2 - 1 is V11() real integer ext-real Element of REAL
- 1 is V11() real integer ext-real non positive set
2 + (- 1) is V11() real integer ext-real set
(len x) - 1 is V11() real integer ext-real Element of REAL
(len x) + (- 1) is V11() real integer ext-real set
len (x /^ 1) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
Seg (len (x /^ 1)) is V45() V46() V47() V48() V49() V50() V58() V65( len (x /^ 1)) bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len (x /^ 1) ) } is set
dom (x /^ 1) is V45() V46() V47() V48() V49() V50() V58() bounded_below bounded_above real-bounded Element of K6(NAT)
(x /^ 1) . (len (x /^ 1)) is V11() real ext-real Element of REAL
(len (x /^ 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
x . ((len (x /^ 1)) + 1) is V11() real ext-real Element of REAL
((len x) - 1) + 1 is V11() real integer ext-real Element of REAL
x . (((len x) - 1) + 1) is V11() real ext-real Element of REAL
rng x is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
rng (x /^ 1) is V45() V46() V47() V58() bounded_below bounded_above real-bounded Element of K6(REAL)
R is non empty Relation-like NAT -defined divs ['f,b'] -valued Function-like total quasi_total Element of K6(K7(NAT,(divs ['f,b'])))
x is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R . x is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
e is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
dom e is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
N . x is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
p is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
p /^ 1 is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
2 - 1 is V11() real integer ext-real Element of REAL
- 1 is V11() real integer ext-real non positive set
2 + (- 1) is V11() real integer ext-real set
len p is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len p) - 1 is V11() real integer ext-real Element of REAL
(len p) + (- 1) is V11() real integer ext-real set
N is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
len N is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
N is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
len N is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len p) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len p) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len p ) } is set
dom p is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
rng p is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
p . 1 is V11() real ext-real Element of REAL
N is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
len N is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
p . 2 is V11() real ext-real Element of REAL
len e is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len e) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len e) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len e ) } is set
e . 1 is V11() real ext-real Element of REAL
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
p . (1 + 1) is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
e . N is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
e . N is V11() real ext-real Element of REAL
chi (['a,f'],['a,f']) is Relation-like ['a,f'] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,f'],REAL))
chi (['f,b'],['f,b']) is Relation-like ['f,b'] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['f,b'],REAL))
divs ['a,f'] is non empty set
K7(NAT,(divs ['a,f'])) is V2() Relation-like V58() set
K6(K7(NAT,(divs ['a,f']))) is V2() V58() set
p is non empty Relation-like NAT -defined divs ['a,f'] -valued Function-like total quasi_total Element of K6(K7(NAT,(divs ['a,f'])))
delta p 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))
lim (delta p) is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R . N is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
q is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
len q is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
N . N is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
r /^ 1 is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
len r is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
2 - 1 is V11() real integer ext-real Element of REAL
- 1 is V11() real integer ext-real non positive set
2 + (- 1) is V11() real integer ext-real set
(len r) - 1 is V11() real integer ext-real Element of REAL
(len r) + (- 1) is V11() real integer ext-real set
n is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
len n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
integral (x0,['f,b']) is V11() real ext-real Element of REAL
integral (x0 || ['f,b']) is V11() real ext-real Element of REAL
upper_integral (x0 || ['f,b']) is V11() real ext-real Element of REAL
upper_sum_set (x0 || ['f,b']) is non empty Relation-like divs ['f,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['f,b']),REAL))
K7((divs ['f,b']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['f,b']),REAL)) is V2() V58() set
rng (upper_sum_set (x0 || ['f,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (x0 || ['f,b']))) is V11() real ext-real Element of REAL
integral (x0,['a,f']) is V11() real ext-real Element of REAL
integral (x0 || ['a,f']) is V11() real ext-real Element of REAL
upper_integral (x0 || ['a,f']) is V11() real ext-real Element of REAL
upper_sum_set (x0 || ['a,f']) is non empty Relation-like divs ['a,f'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,f']),REAL))
K7((divs ['a,f']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['a,f']),REAL)) is V2() V58() set
rng (upper_sum_set (x0 || ['a,f'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (x0 || ['a,f']))) is V11() real ext-real Element of REAL
lower_bound [.a,b.] is V11() real ext-real Element of REAL
upper_bound [.a,b.] is V11() real ext-real Element of REAL
[.(lower_bound [.a,b.]),(upper_bound [.a,b.]).] is V45() V46() V47() closed interval Element of K6(REAL)
upper_bound ['a,b'] is V11() real ext-real Element of REAL
divs ['a,b'] is non empty set
N is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
p . N is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
R . N is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
q is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
q ^ r is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
len r is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len r) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len r) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len r ) } is set
m is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
len m is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom r is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
rng q is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
m is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
dom (q ^ r) is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
x is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
len (q ^ r) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len q is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len q) + (len r) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
x - (len q) is V11() real integer ext-real Element of REAL
- (len q) is V11() real integer ext-real non positive set
x + (- (len q)) is V11() real integer ext-real set
(q ^ r) . x is V11() real ext-real Element of REAL
r . (x - (len q)) is V11() real ext-real Element of REAL
(len q) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V58() V63() set
((len q) + 1) + x1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
S1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
1 + S1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
m - (len q) is V11() real integer ext-real Element of REAL
m + (- (len q)) is V11() real integer ext-real set
S2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V58() V63() set
((len q) + 1) + S2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
1 + k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(q ^ r) . m is V11() real ext-real Element of REAL
r . (m - (len q)) is V11() real ext-real Element of REAL
dom q is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
q . m is V11() real ext-real Element of REAL
S2 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
dom S2 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
q . x is V11() real ext-real Element of REAL
rng r is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
(rng q) \/ (rng r) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
['a,f'] \/ ['f,b'] is non empty V45() V46() V47() Element of K6(REAL)
rng (q ^ r) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
(q ^ r) . (len (q ^ r)) is V11() real ext-real Element of REAL
(q ^ r) . ((len q) + (len r)) is V11() real ext-real Element of REAL
r . (len r) is V11() real ext-real Element of REAL
K7(NAT,(divs ['a,b'])) is V2() Relation-like V58() set
K6(K7(NAT,(divs ['a,b']))) is V2() V58() set
N is non empty Relation-like NAT -defined divs ['a,b'] -valued Function-like total quasi_total Element of K6(K7(NAT,(divs ['a,b'])))
lower_bound ['a,b'] is V11() real ext-real Element of REAL
q is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
p . q is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
r is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
N . q is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,b']
divset ((N . q),r) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
divset ((p . q),r) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
n is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
len n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len n) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len n) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len n ) } is set
lower_bound (divset ((p . q),r)) is V11() real ext-real Element of REAL
upper_bound (divset ((p . q),r)) is V11() real ext-real Element of REAL
[.(lower_bound (divset ((p . q),r))),(upper_bound (divset ((p . q),r))).] is V45() V46() V47() closed interval Element of K6(REAL)
R . q is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
x is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
x1 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
x ^ x1 is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
dom x is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
m is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,b']
len m is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len x1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len x) + (len x1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len x) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len x) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len x ) } is set
Seg (len m) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len m) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len m ) } is set
dom m is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
lower_bound (divset ((N . q),r)) is V11() real ext-real Element of REAL
upper_bound (divset ((N . q),r)) is V11() real ext-real Element of REAL
[.(lower_bound (divset ((N . q),r))),(upper_bound (divset ((N . q),r))).] is V45() V46() V47() closed interval Element of K6(REAL)
r - 1 is V11() real integer ext-real Element of REAL
- 1 is V11() real integer ext-real non positive set
r + (- 1) is V11() real integer ext-real set
r - 0 is V11() real integer ext-real non negative Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued functional integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V46() V47() V48() V49() V50() V51() V58() V59() V62() V63() V65( {} ) FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval set
r + (- 0) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V58() V63() set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
2 - 1 is V11() real integer ext-real Element of REAL
2 + (- 1) is V11() real integer ext-real set
m . (r - 1) is V11() real ext-real Element of REAL
[.(m . (r - 1)),(upper_bound (divset ((N . q),r))).] is V45() V46() V47() closed interval Element of K6(REAL)
m . r is V11() real ext-real Element of REAL
[.(m . (r - 1)),(m . r).] is V45() V46() V47() closed interval Element of K6(REAL)
x . r is V11() real ext-real Element of REAL
[.(m . (r - 1)),(x . r).] is V45() V46() V47() closed interval Element of K6(REAL)
x . (r - 1) is V11() real ext-real Element of REAL
[.(x . (r - 1)),(x . r).] is V45() V46() V47() closed interval Element of K6(REAL)
[.(lower_bound (divset ((p . q),r))),(x . r).] is V45() V46() V47() closed interval Element of K6(REAL)
[.(lower_bound ['a,b']),(upper_bound (divset ((N . q),r))).] is V45() V46() V47() closed interval Element of K6(REAL)
[.(lower_bound ['a,b']),(m . r).] is V45() V46() V47() closed interval Element of K6(REAL)
[.(lower_bound ['a,b']),(x . r).] is V45() V46() V47() closed interval Element of K6(REAL)
x . 1 is V11() real ext-real Element of REAL
[.(lower_bound (divset ((p . q),r))),(x . 1).] is V45() V46() V47() closed interval Element of K6(REAL)
upper_bound ['a,f'] is V11() real ext-real Element of REAL
q is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
p . q is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
R . q is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
r is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
N . q is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,b']
divset ((R . q),r) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
n is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
len n is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len n) + r is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
divset ((N . q),((len n) + r)) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
m is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
len m is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len m) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len m) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len m ) } is set
x1 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
S1 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
x1 ^ S1 is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
dom S1 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
len x1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len x1) + r is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
x is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,b']
dom x is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
lower_bound (divset ((R . q),r)) is V11() real ext-real Element of REAL
upper_bound (divset ((R . q),r)) is V11() real ext-real Element of REAL
[.(lower_bound (divset ((R . q),r))),(upper_bound (divset ((R . q),r))).] is V45() V46() V47() closed interval Element of K6(REAL)
divset ((N . q),((len x1) + r)) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
lower_bound (divset ((N . q),((len x1) + r))) is V11() real ext-real Element of REAL
upper_bound (divset ((N . q),((len x1) + r))) is V11() real ext-real Element of REAL
[.(lower_bound (divset ((N . q),((len x1) + r)))),(upper_bound (divset ((N . q),((len x1) + r)))).] is V45() V46() V47() closed interval Element of K6(REAL)
len S1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
r - 1 is V11() real integer ext-real Element of REAL
- 1 is V11() real integer ext-real non positive set
r + (- 1) is V11() real integer ext-real set
r - 0 is V11() real integer ext-real non negative Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued functional integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V46() V47() V48() V49() V50() V51() V58() V59() V62() V63() V65( {} ) FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval set
r + (- 0) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V58() V63() set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
2 - 1 is V11() real integer ext-real Element of REAL
2 + (- 1) is V11() real integer ext-real set
Seg (len S1) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len S1) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len S1 ) } is set
r + (len x1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
((len x1) + r) - 1 is V11() real integer ext-real Element of REAL
((len x1) + r) + (- 1) is V11() real integer ext-real set
x . (((len x1) + r) - 1) is V11() real ext-real Element of REAL
[.(x . (((len x1) + r) - 1)),(upper_bound (divset ((N . q),((len x1) + r)))).] is V45() V46() V47() closed interval Element of K6(REAL)
x . ((len x1) + r) is V11() real ext-real Element of REAL
[.(x . (((len x1) + r) - 1)),(x . ((len x1) + r)).] is V45() V46() V47() closed interval Element of K6(REAL)
(len x1) + (r - 1) is V11() real integer ext-real Element of REAL
x . ((len x1) + (r - 1)) is V11() real ext-real Element of REAL
S1 . r is V11() real ext-real Element of REAL
[.(x . ((len x1) + (r - 1))),(S1 . r).] is V45() V46() V47() closed interval Element of K6(REAL)
S1 . (r - 1) is V11() real ext-real Element of REAL
[.(S1 . (r - 1)),(S1 . r).] is V45() V46() V47() closed interval Element of K6(REAL)
[.(lower_bound (divset ((R . q),r))),(S1 . r).] is V45() V46() V47() closed interval Element of K6(REAL)
Seg (len x1) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len x1) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len x1 ) } is set
dom x1 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
x1 . (len x1) is V11() real ext-real Element of REAL
[.(x1 . (len x1)),(upper_bound (divset ((N . q),((len x1) + r)))).] is V45() V46() V47() closed interval Element of K6(REAL)
[.(upper_bound ['a,f']),(upper_bound (divset ((N . q),((len x1) + r)))).] is V45() V46() V47() closed interval Element of K6(REAL)
[.(lower_bound ['f,b']),(x . ((len x1) + r)).] is V45() V46() V47() closed interval Element of K6(REAL)
[.(lower_bound ['f,b']),(S1 . r).] is V45() V46() V47() closed interval Element of K6(REAL)
S1 . 1 is V11() real ext-real Element of REAL
[.(lower_bound (divset ((R . q),r))),(S1 . 1).] is V45() V46() V47() closed interval Element of K6(REAL)
chi (['a,b'],['a,b']) is Relation-like ['a,b'] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
r is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
R . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
divset ((R . r),n) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
m is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
len m is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len m) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len m) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len m ) } is set
dom m is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
x0 | ['a,f'] is Relation-like REAL -defined ['a,f'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(x0 || ['a,f']) | ['a,f'] is Relation-like ['a,f'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,f'],REAL))
r is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
p . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
divset ((p . r),n) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
m is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
len m is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len m) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len m) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len m ) } is set
dom m is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
N . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,b']
upper_volume ((x0 || ['a,b']),(N . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
p . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
upper_volume ((x0 || ['a,f']),(p . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
R . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
upper_volume ((x0 || ['f,b']),(R . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
(upper_volume ((x0 || ['a,f']),(p . r))) ^ (upper_volume ((x0 || ['f,b']),(R . r))) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
S1 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
S2 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
S1 ^ S2 is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
n is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
len n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
x1 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,b']
len x1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len S1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len S2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len S1) + (len S2) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
m is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
len m is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(len m) + (len S2) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
x is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
len x is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(len m) + (len x) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V58() V63() set
dom x is V45() V46() V47() V48() V49() V50() V58() bounded_below bounded_above real-bounded Element of K6(NAT)
Seg (len x) is V45() V46() V47() V48() V49() V50() V58() V65( len x) bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len x ) } is set
1 + (len m) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
k + (len m) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(len m) + k is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
Seg (len n) is V45() V46() V47() V48() V49() V50() V58() V65( len n) bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len n ) } is set
Seg (len x1) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len x1) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len x1 ) } is set
dom x1 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
n . ((len m) + k) is V11() real ext-real Element of REAL
divset ((N . r),((len m) + k)) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
(x0 || ['a,b']) | (divset ((N . r),((len m) + k))) is Relation-like ['a,b'] -defined divset ((N . r),((len m) + k)) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
rng ((x0 || ['a,b']) | (divset ((N . r),((len m) + k)))) is V45() V46() V47() Element of K6(REAL)
upper_bound (rng ((x0 || ['a,b']) | (divset ((N . r),((len m) + k))))) is V11() real ext-real Element of REAL
vol (divset ((N . r),((len m) + k))) is V11() real ext-real Element of REAL
upper_bound (divset ((N . r),((len m) + k))) is V11() real ext-real Element of REAL
lower_bound (divset ((N . r),((len m) + k))) is V11() real ext-real Element of REAL
(upper_bound (divset ((N . r),((len m) + k)))) - (lower_bound (divset ((N . r),((len m) + k)))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((N . r),((len m) + k)))) is V11() real ext-real set
(upper_bound (divset ((N . r),((len m) + k)))) + (- (lower_bound (divset ((N . r),((len m) + k))))) is V11() real ext-real set
(upper_bound (rng ((x0 || ['a,b']) | (divset ((N . r),((len m) + k)))))) * (vol (divset ((N . r),((len m) + k)))) is V11() real ext-real Element of REAL
Seg (len S2) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len S2) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len S2 ) } is set
dom S2 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
divset ((R . r),k) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
(x0 || ['f,b']) | (divset ((R . r),k)) is Relation-like ['f,b'] -defined divset ((R . r),k) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['f,b'],REAL))
rng ((x0 || ['f,b']) | (divset ((R . r),k))) is V45() V46() V47() Element of K6(REAL)
upper_bound (rng ((x0 || ['f,b']) | (divset ((R . r),k)))) is V11() real ext-real Element of REAL
vol (divset ((R . r),k)) is V11() real ext-real Element of REAL
upper_bound (divset ((R . r),k)) is V11() real ext-real Element of REAL
lower_bound (divset ((R . r),k)) is V11() real ext-real Element of REAL
(upper_bound (divset ((R . r),k))) - (lower_bound (divset ((R . r),k))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((R . r),k))) is V11() real ext-real set
(upper_bound (divset ((R . r),k))) + (- (lower_bound (divset ((R . r),k)))) is V11() real ext-real set
(upper_bound (rng ((x0 || ['f,b']) | (divset ((R . r),k))))) * (vol (divset ((R . r),k))) is V11() real ext-real Element of REAL
x . k is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V58() V63() set
dom m is V45() V46() V47() V48() V49() V50() V58() bounded_below bounded_above real-bounded Element of K6(NAT)
Seg (len m) is V45() V46() V47() V48() V49() V50() V58() V65( len m) bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len m ) } is set
Seg (len S1) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len S1) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len S1 ) } is set
dom S1 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
n . k is V11() real ext-real Element of REAL
divset ((N . r),k) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
(x0 || ['a,b']) | (divset ((N . r),k)) is Relation-like ['a,b'] -defined divset ((N . r),k) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
rng ((x0 || ['a,b']) | (divset ((N . r),k))) is V45() V46() V47() Element of K6(REAL)
upper_bound (rng ((x0 || ['a,b']) | (divset ((N . r),k)))) is V11() real ext-real Element of REAL
vol (divset ((N . r),k)) is V11() real ext-real Element of REAL
upper_bound (divset ((N . r),k)) is V11() real ext-real Element of REAL
lower_bound (divset ((N . r),k)) is V11() real ext-real Element of REAL
(upper_bound (divset ((N . r),k))) - (lower_bound (divset ((N . r),k))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((N . r),k))) is V11() real ext-real set
(upper_bound (divset ((N . r),k))) + (- (lower_bound (divset ((N . r),k)))) is V11() real ext-real set
(upper_bound (rng ((x0 || ['a,b']) | (divset ((N . r),k))))) * (vol (divset ((N . r),k))) is V11() real ext-real Element of REAL
divset ((p . r),k) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
(x0 || ['a,f']) | (divset ((p . r),k)) is Relation-like ['a,f'] -defined divset ((p . r),k) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,f'],REAL))
rng ((x0 || ['a,f']) | (divset ((p . r),k))) is V45() V46() V47() Element of K6(REAL)
upper_bound (rng ((x0 || ['a,f']) | (divset ((p . r),k)))) is V11() real ext-real Element of REAL
vol (divset ((p . r),k)) is V11() real ext-real Element of REAL
upper_bound (divset ((p . r),k)) is V11() real ext-real Element of REAL
lower_bound (divset ((p . r),k)) is V11() real ext-real Element of REAL
(upper_bound (divset ((p . r),k))) - (lower_bound (divset ((p . r),k))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((p . r),k))) is V11() real ext-real set
(upper_bound (divset ((p . r),k))) + (- (lower_bound (divset ((p . r),k)))) is V11() real ext-real set
(upper_bound (rng ((x0 || ['a,f']) | (divset ((p . r),k))))) * (vol (divset ((p . r),k))) is V11() real ext-real Element of REAL
m . k is V11() real ext-real Element of REAL
dom n is V45() V46() V47() V48() V49() V50() V58() bounded_below bounded_above real-bounded Element of K6(NAT)
Seg ((len m) + (len x)) is V45() V46() V47() V48() V49() V50() V58() V65((len m) + (len x)) bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= (len m) + (len x) ) } is set
r is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
N . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,b']
upper_volume ((x0 || ['a,b']),(N . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (upper_volume ((x0 || ['a,b']),(N . r))) is V11() real ext-real Element of REAL
p . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
upper_volume ((x0 || ['a,f']),(p . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (upper_volume ((x0 || ['a,f']),(p . r))) is V11() real ext-real Element of REAL
R . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
upper_volume ((x0 || ['f,b']),(R . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (upper_volume ((x0 || ['f,b']),(R . r))) is V11() real ext-real Element of REAL
(Sum (upper_volume ((x0 || ['a,f']),(p . r)))) + (Sum (upper_volume ((x0 || ['f,b']),(R . r)))) is V11() real ext-real Element of REAL
(upper_volume ((x0 || ['a,f']),(p . r))) ^ (upper_volume ((x0 || ['f,b']),(R . r))) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
upper_sum ((x0 || ['a,b']),N) 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))
r is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(upper_sum ((x0 || ['a,b']),N)) . r is V11() real ext-real Element of REAL
N . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,b']
upper_sum ((x0 || ['a,b']),(N . r)) is V11() real ext-real Element of REAL
upper_volume ((x0 || ['a,b']),(N . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (upper_volume ((x0 || ['a,b']),(N . r))) is V11() real ext-real Element of REAL
p . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
upper_sum ((x0 || ['a,f']),(p . r)) is V11() real ext-real Element of REAL
upper_volume ((x0 || ['a,f']),(p . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (upper_volume ((x0 || ['a,f']),(p . r))) is V11() real ext-real Element of REAL
R . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
upper_volume ((x0 || ['f,b']),(R . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (upper_volume ((x0 || ['f,b']),(R . r))) is V11() real ext-real Element of REAL
(upper_sum ((x0 || ['a,f']),(p . r))) + (Sum (upper_volume ((x0 || ['f,b']),(R . r)))) is V11() real ext-real Element of REAL
upper_sum ((x0 || ['a,f']),p) 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))
(upper_sum ((x0 || ['a,f']),p)) . r is V11() real ext-real Element of REAL
upper_sum ((x0 || ['f,b']),(R . r)) is V11() real ext-real Element of REAL
((upper_sum ((x0 || ['a,f']),p)) . r) + (upper_sum ((x0 || ['f,b']),(R . r))) is V11() real ext-real Element of REAL
upper_sum ((x0 || ['f,b']),R) 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))
(upper_sum ((x0 || ['f,b']),R)) . r is V11() real ext-real Element of REAL
((upper_sum ((x0 || ['a,f']),p)) . r) + ((upper_sum ((x0 || ['f,b']),R)) . r) is V11() real ext-real Element of REAL
(upper_sum ((x0 || ['a,f']),p)) + (upper_sum ((x0 || ['f,b']),R)) 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))
lower_integral (x0 || ['f,b']) is V11() real ext-real Element of REAL
lower_sum_set (x0 || ['f,b']) is non empty Relation-like divs ['f,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['f,b']),REAL))
rng (lower_sum_set (x0 || ['f,b'])) is non empty V45() V46() V47() Element of K6(REAL)
upper_bound (rng (lower_sum_set (x0 || ['f,b']))) is V11() real ext-real Element of REAL
r is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
x + R is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(delta L) . (x + R) is V11() real ext-real Element of REAL
((delta L) . (x + R)) - 0 is V11() real ext-real Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued functional integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V46() V47() V48() V49() V50() V51() V58() V59() V62() V63() V65( {} ) FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval set
((delta L) . (x + R)) + (- 0) is V11() real ext-real set
abs (((delta L) . (x + R)) - 0) is V11() real ext-real Element of REAL
L . (x + R) is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
delta (L . (x + R)) is V11() real ext-real Element of REAL
upper_volume ((chi (['f,b'],['f,b'])),(L . (x + R))) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (upper_volume ((chi (['f,b'],['f,b'])),(L . (x + R)))) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
sup (rng (upper_volume ((chi (['f,b'],['f,b'])),(L . (x + R))))) is V11() real ext-real set
(delta (L . (x + R))) - 0 is V11() real ext-real Element of REAL
(delta (L . (x + R))) + (- 0) is V11() real ext-real set
abs ((delta (L . (x + R))) - 0) is V11() real ext-real Element of REAL
N . x is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
delta N 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))
(delta N) . x is V11() real ext-real Element of REAL
((delta N) . x) - 0 is V11() real ext-real Element of REAL
((delta N) . x) + (- 0) is V11() real ext-real set
abs (((delta N) . x) - 0) is V11() real ext-real Element of REAL
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
S1 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
x1 + R is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
L . (x1 + R) is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
r is V11() real ext-real set
r / 2 is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative set
r * (2 ") is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(delta N) . x is V11() real ext-real Element of REAL
((delta N) . x) - 0 is V11() real ext-real Element of REAL
((delta N) . x) + (- 0) is V11() real ext-real set
abs (((delta N) . x) - 0) is V11() real ext-real Element of REAL
N . x is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
delta (N . x) is V11() real ext-real Element of REAL
upper_volume ((chi (['f,b'],['f,b'])),(N . x)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (upper_volume ((chi (['f,b'],['f,b'])),(N . x))) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
sup (rng (upper_volume ((chi (['f,b'],['f,b'])),(N . x)))) is V11() real ext-real set
abs (delta (N . x)) is V11() real ext-real Element of REAL
R . x is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
upper_volume ((chi (['f,b'],['f,b'])),(R . x)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (upper_volume ((chi (['f,b'],['f,b'])),(R . x))) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
S1 is V11() real ext-real set
dom (upper_volume ((chi (['f,b'],['f,b'])),(R . x))) is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
S2 is set
(upper_volume ((chi (['f,b'],['f,b'])),(R . x))) . S2 is V11() real ext-real Element of REAL
len (upper_volume ((chi (['f,b'],['f,b'])),(R . x))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len (upper_volume ((chi (['f,b'],['f,b'])),(R . x)))) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len (upper_volume ((chi (['f,b'],['f,b'])),(R . x)))) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len (upper_volume ((chi (['f,b'],['f,b'])),(R . x))) ) } is set
x is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
len x is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
S1 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
S1 /^ 1 is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
x1 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
len x1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len S1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len S1) - 1 is V11() real integer ext-real Element of REAL
- 1 is V11() real integer ext-real non positive set
(len S1) + (- 1) is V11() real integer ext-real set
dom x1 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
len (upper_volume ((chi (['f,b'],['f,b'])),(N . x))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len (upper_volume ((chi (['f,b'],['f,b'])),(N . x)))) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len (upper_volume ((chi (['f,b'],['f,b'])),(N . x)))) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len (upper_volume ((chi (['f,b'],['f,b'])),(N . x))) ) } is set
dom (upper_volume ((chi (['f,b'],['f,b'])),(N . x))) is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
(upper_volume ((chi (['f,b'],['f,b'])),(N . x))) . 2 is V11() real ext-real Element of REAL
(len x1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len (upper_volume ((chi (['f,b'],['f,b'])),(R . x)))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(upper_volume ((chi (['f,b'],['f,b'])),(N . x))) . 1 is V11() real ext-real Element of REAL
dom S1 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
Seg (len S1) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len S1) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len S1 ) } is set
divset ((N . x),1) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
lower_bound (divset ((N . x),1)) is V11() real ext-real Element of REAL
upper_bound (divset ((N . x),1)) is V11() real ext-real Element of REAL
[.(lower_bound (divset ((N . x),1))),(upper_bound (divset ((N . x),1))).] is V45() V46() V47() closed interval Element of K6(REAL)
[.(lower_bound ['f,b']),(upper_bound (divset ((N . x),1))).] is V45() V46() V47() closed interval Element of K6(REAL)
lower_bound [.(lower_bound ['f,b']),(upper_bound (divset ((N . x),1))).] is V11() real ext-real Element of REAL
upper_bound [.(lower_bound ['f,b']),(upper_bound (divset ((N . x),1))).] is V11() real ext-real Element of REAL
[.(lower_bound [.(lower_bound ['f,b']),(upper_bound (divset ((N . x),1))).]),(upper_bound [.(lower_bound ['f,b']),(upper_bound (divset ((N . x),1))).]).] is V45() V46() V47() closed interval Element of K6(REAL)
divset ((R . x),k) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
divset ((R . x),1) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
lower_bound (divset ((R . x),1)) is V11() real ext-real Element of REAL
upper_bound (divset ((R . x),1)) is V11() real ext-real Element of REAL
[.(lower_bound (divset ((R . x),1))),(upper_bound (divset ((R . x),1))).] is V45() V46() V47() closed interval Element of K6(REAL)
[.(lower_bound ['f,b']),(upper_bound (divset ((R . x),1))).] is V45() V46() V47() closed interval Element of K6(REAL)
x1 . 1 is V11() real ext-real Element of REAL
[.(lower_bound ['f,b']),(x1 . 1).] is V45() V46() V47() closed interval Element of K6(REAL)
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
S1 . (1 + 1) is V11() real ext-real Element of REAL
[.(lower_bound ['f,b']),(S1 . (1 + 1)).] is V45() V46() V47() closed interval Element of K6(REAL)
divset ((N . x),2) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
upper_bound (divset ((N . x),2)) is V11() real ext-real Element of REAL
[.(lower_bound ['f,b']),(upper_bound (divset ((N . x),2))).] is V45() V46() V47() closed interval Element of K6(REAL)
lower_bound [.(lower_bound ['f,b']),(upper_bound (divset ((N . x),2))).] is V11() real ext-real Element of REAL
upper_bound [.(lower_bound ['f,b']),(upper_bound (divset ((N . x),2))).] is V11() real ext-real Element of REAL
[.(lower_bound [.(lower_bound ['f,b']),(upper_bound (divset ((N . x),2))).]),(upper_bound [.(lower_bound ['f,b']),(upper_bound (divset ((N . x),2))).]).] is V45() V46() V47() closed interval Element of K6(REAL)
vol (divset ((R . x),1)) is V11() real ext-real Element of REAL
(upper_bound (divset ((R . x),1))) - (lower_bound (divset ((R . x),1))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((R . x),1))) is V11() real ext-real set
(upper_bound (divset ((R . x),1))) + (- (lower_bound (divset ((R . x),1)))) is V11() real ext-real set
(upper_bound (divset ((N . x),2))) - (upper_bound (divset ((N . x),1))) is V11() real ext-real Element of REAL
- (upper_bound (divset ((N . x),1))) is V11() real ext-real set
(upper_bound (divset ((N . x),2))) + (- (upper_bound (divset ((N . x),1)))) is V11() real ext-real set
(upper_bound [.(lower_bound ['f,b']),(upper_bound (divset ((N . x),1))).]) - (lower_bound ['f,b']) is V11() real ext-real Element of REAL
- (lower_bound ['f,b']) is V11() real ext-real set
(upper_bound [.(lower_bound ['f,b']),(upper_bound (divset ((N . x),1))).]) + (- (lower_bound ['f,b'])) is V11() real ext-real set
((upper_bound (divset ((N . x),2))) - (upper_bound (divset ((N . x),1)))) + ((upper_bound [.(lower_bound ['f,b']),(upper_bound (divset ((N . x),1))).]) - (lower_bound ['f,b'])) is V11() real ext-real Element of REAL
vol (divset ((N . x),1)) is V11() real ext-real Element of REAL
(upper_bound (divset ((N . x),1))) - (lower_bound (divset ((N . x),1))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((N . x),1))) is V11() real ext-real set
(upper_bound (divset ((N . x),1))) + (- (lower_bound (divset ((N . x),1)))) is V11() real ext-real set
((upper_bound (divset ((N . x),2))) - (upper_bound (divset ((N . x),1)))) + (vol (divset ((N . x),1))) is V11() real ext-real Element of REAL
lower_bound (divset ((N . x),2)) is V11() real ext-real Element of REAL
[.(lower_bound (divset ((N . x),2))),(upper_bound (divset ((N . x),2))).] is V45() V46() V47() closed interval Element of K6(REAL)
2 - 1 is V11() real integer ext-real Element of REAL
2 + (- 1) is V11() real integer ext-real set
S1 . (2 - 1) is V11() real ext-real Element of REAL
[.(S1 . (2 - 1)),(upper_bound (divset ((N . x),2))).] is V45() V46() V47() closed interval Element of K6(REAL)
[.(upper_bound (divset ((N . x),1))),(upper_bound (divset ((N . x),2))).] is V45() V46() V47() closed interval Element of K6(REAL)
lower_bound [.(upper_bound (divset ((N . x),1))),(upper_bound (divset ((N . x),2))).] is V11() real ext-real Element of REAL
upper_bound [.(upper_bound (divset ((N . x),1))),(upper_bound (divset ((N . x),2))).] is V11() real ext-real Element of REAL
[.(lower_bound [.(upper_bound (divset ((N . x),1))),(upper_bound (divset ((N . x),2))).]),(upper_bound [.(upper_bound (divset ((N . x),1))),(upper_bound (divset ((N . x),2))).]).] is V45() V46() V47() closed interval Element of K6(REAL)
vol (divset ((N . x),2)) is V11() real ext-real Element of REAL
(upper_bound (divset ((N . x),2))) - (lower_bound (divset ((N . x),2))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((N . x),2))) is V11() real ext-real set
(upper_bound (divset ((N . x),2))) + (- (lower_bound (divset ((N . x),2)))) is V11() real ext-real set
(vol (divset ((N . x),2))) + (vol (divset ((N . x),1))) is V11() real ext-real Element of REAL
((upper_volume ((chi (['f,b'],['f,b'])),(N . x))) . 2) + (vol (divset ((N . x),1))) is V11() real ext-real Element of REAL
((upper_volume ((chi (['f,b'],['f,b'])),(N . x))) . 2) + ((upper_volume ((chi (['f,b'],['f,b'])),(N . x))) . 1) is V11() real ext-real Element of REAL
(r / 2) + (r / 2) is V11() real ext-real Element of REAL
(chi (['f,b'],['f,b'])) | (divset ((R . x),k)) is Relation-like ['f,b'] -defined divset ((R . x),k) -defined ['f,b'] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['f,b'],REAL))
rng ((chi (['f,b'],['f,b'])) | (divset ((R . x),k))) is V45() V46() V47() Element of K6(REAL)
upper_bound (rng ((chi (['f,b'],['f,b'])) | (divset ((R . x),k)))) is V11() real ext-real Element of REAL
vol (divset ((R . x),k)) is V11() real ext-real Element of REAL
upper_bound (divset ((R . x),k)) is V11() real ext-real Element of REAL
lower_bound (divset ((R . x),k)) is V11() real ext-real Element of REAL
(upper_bound (divset ((R . x),k))) - (lower_bound (divset ((R . x),k))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((R . x),k))) is V11() real ext-real set
(upper_bound (divset ((R . x),k))) + (- (lower_bound (divset ((R . x),k)))) is V11() real ext-real set
(upper_bound (rng ((chi (['f,b'],['f,b'])) | (divset ((R . x),k))))) * (vol (divset ((R . x),k))) is V11() real ext-real Element of REAL
Seg ((len x1) + 1) is non empty V45() V46() V47() V48() V49() V50() V58() V65((len x1) + 1) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= (len x1) + 1 ) } is set
Seg (len x1) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len x1) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len x1 ) } is set
k - 1 is V11() real integer ext-real Element of REAL
k + (- 1) is V11() real integer ext-real set
[.(lower_bound (divset ((R . x),k))),(upper_bound (divset ((R . x),k))).] is V45() V46() V47() closed interval Element of K6(REAL)
x1 . (k - 1) is V11() real ext-real Element of REAL
[.(x1 . (k - 1)),(upper_bound (divset ((R . x),k))).] is V45() V46() V47() closed interval Element of K6(REAL)
x1 . k is V11() real ext-real Element of REAL
[.(x1 . (k - 1)),(x1 . k).] is V45() V46() V47() closed interval Element of K6(REAL)
S2 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
S2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
S1 . (S2 + 1) is V11() real ext-real Element of REAL
[.(S1 . (S2 + 1)),(x1 . k).] is V45() V46() V47() closed interval Element of K6(REAL)
(k - 1) + 1 is V11() real integer ext-real Element of REAL
S1 . ((k - 1) + 1) is V11() real ext-real Element of REAL
S1 . (k + 1) is V11() real ext-real Element of REAL
[.(S1 . ((k - 1) + 1)),(S1 . (k + 1)).] is V45() V46() V47() closed interval Element of K6(REAL)
(k + 1) - 1 is V11() real integer ext-real Element of REAL
(k + 1) + (- 1) is V11() real integer ext-real set
S1 . ((k + 1) - 1) is V11() real ext-real Element of REAL
divset ((N . x),(k + 1)) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
upper_bound (divset ((N . x),(k + 1))) is V11() real ext-real Element of REAL
[.(S1 . ((k + 1) - 1)),(upper_bound (divset ((N . x),(k + 1)))).] is V45() V46() V47() closed interval Element of K6(REAL)
lower_bound (divset ((N . x),(k + 1))) is V11() real ext-real Element of REAL
[.(lower_bound (divset ((N . x),(k + 1)))),(upper_bound (divset ((N . x),(k + 1)))).] is V45() V46() V47() closed interval Element of K6(REAL)
(upper_volume ((chi (['f,b'],['f,b'])),(N . x))) . (k + 1) is V11() real ext-real Element of REAL
sup (rng (upper_volume ((chi (['f,b'],['f,b'])),(R . x)))) is V11() real ext-real set
delta (R . x) is V11() real ext-real Element of REAL
abs (delta (R . x)) is V11() real ext-real Element of REAL
delta R 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))
(delta R) . x is V11() real ext-real Element of REAL
((delta R) . x) - 0 is V11() real ext-real Element of REAL
((delta R) . x) + (- 0) is V11() real ext-real set
abs (((delta R) . x) - 0) is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(delta R) . x is V11() real ext-real Element of REAL
((delta R) . x) - 0 is V11() real ext-real Element of REAL
((delta R) . x) + (- 0) is V11() real ext-real set
abs (((delta R) . x) - 0) is V11() real ext-real Element of REAL
lim (delta R) is V11() real ext-real Element of REAL
lim (upper_sum ((x0 || ['f,b']),R)) is V11() real ext-real Element of REAL
r is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
max (n,m) is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V58() V63() set
x is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
S1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(delta R) . S1 is V11() real ext-real Element of REAL
((delta R) . S1) - 0 is V11() real ext-real Element of REAL
((delta R) . S1) + (- 0) is V11() real ext-real set
abs (((delta R) . S1) - 0) is V11() real ext-real Element of REAL
R . S1 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
delta (R . S1) is V11() real ext-real Element of REAL
upper_volume ((chi (['f,b'],['f,b'])),(R . S1)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (upper_volume ((chi (['f,b'],['f,b'])),(R . S1))) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
sup (rng (upper_volume ((chi (['f,b'],['f,b'])),(R . S1)))) is V11() real ext-real set
abs (delta (R . S1)) is V11() real ext-real Element of REAL
(delta p) . S1 is V11() real ext-real Element of REAL
((delta p) . S1) - 0 is V11() real ext-real Element of REAL
((delta p) . S1) + (- 0) is V11() real ext-real set
abs (((delta p) . S1) - 0) is V11() real ext-real Element of REAL
p . S1 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
delta (p . S1) is V11() real ext-real Element of REAL
upper_volume ((chi (['a,f'],['a,f'])),(p . S1)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (upper_volume ((chi (['a,f'],['a,f'])),(p . S1))) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
sup (rng (upper_volume ((chi (['a,f'],['a,f'])),(p . S1)))) is V11() real ext-real set
abs (delta (p . S1)) is V11() real ext-real Element of REAL
N . S1 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,b']
upper_volume ((chi (['a,b'],['a,b'])),(N . S1)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
rng (upper_volume ((chi (['a,b'],['a,b'])),(N . S1))) is non empty V45() V46() V47() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
k is V11() real ext-real set
dom (upper_volume ((chi (['a,b'],['a,b'])),(N . S1))) is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
x is set
(upper_volume ((chi (['a,b'],['a,b'])),(N . S1))) . x is V11() real ext-real Element of REAL
len (upper_volume ((chi (['a,b'],['a,b'])),(N . S1))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len (upper_volume ((chi (['a,b'],['a,b'])),(N . S1)))) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len (upper_volume ((chi (['a,b'],['a,b'])),(N . S1)))) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len (upper_volume ((chi (['a,b'],['a,b'])),(N . S1))) ) } is set
i is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
S2 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,b']
len S2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom S2 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
divset ((N . S1),i) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
(chi (['a,b'],['a,b'])) | (divset ((N . S1),i)) is Relation-like ['a,b'] -defined divset ((N . S1),i) -defined ['a,b'] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
rng ((chi (['a,b'],['a,b'])) | (divset ((N . S1),i))) is V45() V46() V47() Element of K6(REAL)
upper_bound (rng ((chi (['a,b'],['a,b'])) | (divset ((N . S1),i)))) is V11() real ext-real Element of REAL
vol (divset ((N . S1),i)) is V11() real ext-real Element of REAL
upper_bound (divset ((N . S1),i)) is V11() real ext-real Element of REAL
lower_bound (divset ((N . S1),i)) is V11() real ext-real Element of REAL
(upper_bound (divset ((N . S1),i))) - (lower_bound (divset ((N . S1),i))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((N . S1),i))) is V11() real ext-real set
(upper_bound (divset ((N . S1),i))) + (- (lower_bound (divset ((N . S1),i)))) is V11() real ext-real set
(upper_bound (rng ((chi (['a,b'],['a,b'])) | (divset ((N . S1),i))))) * (vol (divset ((N . S1),i))) is V11() real ext-real Element of REAL
S1 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
S2 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
S1 ^ S2 is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
len S1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len S2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len S1) + (len S2) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len S1) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len S1) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len S1 ) } is set
dom S1 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
len (upper_volume ((chi (['a,f'],['a,f'])),(p . S1))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom (upper_volume ((chi (['a,f'],['a,f'])),(p . S1))) is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
divset ((p . S1),i) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
(chi (['a,f'],['a,f'])) | (divset ((p . S1),i)) is Relation-like ['a,f'] -defined divset ((p . S1),i) -defined ['a,f'] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,f'],REAL))
(upper_volume ((chi (['a,f'],['a,f'])),(p . S1))) . i is V11() real ext-real Element of REAL
(len S1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V58() V63() set
((len S1) + 1) + k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
1 + k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
i - (len S1) is V11() real integer ext-real Element of REAL
- (len S1) is V11() real integer ext-real non positive set
i + (- (len S1)) is V11() real integer ext-real set
Seg (len S2) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len S2) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len S2 ) } is set
dom S2 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
divset ((R . S1),(1 + k)) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
(len S1) + (1 + k) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
divset ((N . S1),((len S1) + (1 + k))) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
(chi (['f,b'],['f,b'])) | (divset ((R . S1),(1 + k))) is Relation-like ['f,b'] -defined divset ((R . S1),(1 + k)) -defined ['f,b'] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['f,b'],REAL))
rng ((chi (['f,b'],['f,b'])) | (divset ((R . S1),(1 + k)))) is V45() V46() V47() Element of K6(REAL)
upper_bound (rng ((chi (['f,b'],['f,b'])) | (divset ((R . S1),(1 + k))))) is V11() real ext-real Element of REAL
vol (divset ((R . S1),(1 + k))) is V11() real ext-real Element of REAL
upper_bound (divset ((R . S1),(1 + k))) is V11() real ext-real Element of REAL
lower_bound (divset ((R . S1),(1 + k))) is V11() real ext-real Element of REAL
(upper_bound (divset ((R . S1),(1 + k)))) - (lower_bound (divset ((R . S1),(1 + k)))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((R . S1),(1 + k)))) is V11() real ext-real set
(upper_bound (divset ((R . S1),(1 + k)))) + (- (lower_bound (divset ((R . S1),(1 + k))))) is V11() real ext-real set
(upper_bound (rng ((chi (['f,b'],['f,b'])) | (divset ((R . S1),(1 + k)))))) * (vol (divset ((R . S1),(1 + k)))) is V11() real ext-real Element of REAL
(upper_volume ((chi (['f,b'],['f,b'])),(R . S1))) . (1 + k) is V11() real ext-real Element of REAL
len (upper_volume ((chi (['f,b'],['f,b'])),(R . S1))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom (upper_volume ((chi (['f,b'],['f,b'])),(R . S1))) is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
delta (N . S1) is V11() real ext-real Element of REAL
sup (rng (upper_volume ((chi (['a,b'],['a,b'])),(N . S1)))) is V11() real ext-real set
abs (delta (N . S1)) is V11() real ext-real Element of REAL
delta N 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))
(delta N) . S1 is V11() real ext-real Element of REAL
((delta N) . S1) - 0 is V11() real ext-real Element of REAL
((delta N) . S1) + (- 0) is V11() real ext-real set
abs (((delta N) . S1) - 0) is V11() real ext-real Element of REAL
S1 is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(delta N) . S1 is V11() real ext-real Element of REAL
((delta N) . S1) - 0 is V11() real ext-real Element of REAL
((delta N) . S1) + (- 0) is V11() real ext-real set
abs (((delta N) . S1) - 0) is V11() real ext-real Element of REAL
lim (delta N) is V11() real ext-real Element of REAL
(x0 || ['a,b']) | ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
upper_integral (x0 || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set (x0 || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
K7((divs ['a,b']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['a,b']),REAL)) is V2() V58() set
rng (upper_sum_set (x0 || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (x0 || ['a,b']))) is V11() real ext-real Element of REAL
lim (upper_sum ((x0 || ['a,b']),N)) is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
N . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,b']
lower_volume ((x0 || ['a,b']),(N . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
p . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
lower_volume ((x0 || ['a,f']),(p . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
R . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
lower_volume ((x0 || ['f,b']),(R . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
(lower_volume ((x0 || ['a,f']),(p . r))) ^ (lower_volume ((x0 || ['f,b']),(R . r))) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
S1 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
S2 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
S1 ^ S2 is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
n is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
len n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
x1 is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,b']
len x1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len S1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len S2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len S1) + (len S2) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
m is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
len m is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(len m) + (len S2) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
x is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
len x is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(len m) + (len x) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V58() V63() set
dom x is V45() V46() V47() V48() V49() V50() V58() bounded_below bounded_above real-bounded Element of K6(NAT)
Seg (len x) is V45() V46() V47() V48() V49() V50() V58() V65( len x) bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len x ) } is set
1 + (len m) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
k + (len m) is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(len m) + k is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
Seg (len n) is V45() V46() V47() V48() V49() V50() V58() V65( len n) bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len n ) } is set
Seg (len x1) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len x1) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len x1 ) } is set
dom x1 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
n . ((len m) + k) is V11() real ext-real Element of REAL
divset ((N . r),((len m) + k)) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
(x0 || ['a,b']) | (divset ((N . r),((len m) + k))) is Relation-like ['a,b'] -defined divset ((N . r),((len m) + k)) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
rng ((x0 || ['a,b']) | (divset ((N . r),((len m) + k)))) is V45() V46() V47() Element of K6(REAL)
lower_bound (rng ((x0 || ['a,b']) | (divset ((N . r),((len m) + k))))) is V11() real ext-real Element of REAL
vol (divset ((N . r),((len m) + k))) is V11() real ext-real Element of REAL
upper_bound (divset ((N . r),((len m) + k))) is V11() real ext-real Element of REAL
lower_bound (divset ((N . r),((len m) + k))) is V11() real ext-real Element of REAL
(upper_bound (divset ((N . r),((len m) + k)))) - (lower_bound (divset ((N . r),((len m) + k)))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((N . r),((len m) + k)))) is V11() real ext-real set
(upper_bound (divset ((N . r),((len m) + k)))) + (- (lower_bound (divset ((N . r),((len m) + k))))) is V11() real ext-real set
(lower_bound (rng ((x0 || ['a,b']) | (divset ((N . r),((len m) + k)))))) * (vol (divset ((N . r),((len m) + k)))) is V11() real ext-real Element of REAL
Seg (len S2) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len S2) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len S2 ) } is set
dom S2 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
divset ((R . r),k) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
(x0 || ['f,b']) | (divset ((R . r),k)) is Relation-like ['f,b'] -defined divset ((R . r),k) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['f,b'],REAL))
rng ((x0 || ['f,b']) | (divset ((R . r),k))) is V45() V46() V47() Element of K6(REAL)
lower_bound (rng ((x0 || ['f,b']) | (divset ((R . r),k)))) is V11() real ext-real Element of REAL
vol (divset ((R . r),k)) is V11() real ext-real Element of REAL
upper_bound (divset ((R . r),k)) is V11() real ext-real Element of REAL
lower_bound (divset ((R . r),k)) is V11() real ext-real Element of REAL
(upper_bound (divset ((R . r),k))) - (lower_bound (divset ((R . r),k))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((R . r),k))) is V11() real ext-real set
(upper_bound (divset ((R . r),k))) + (- (lower_bound (divset ((R . r),k)))) is V11() real ext-real set
(lower_bound (rng ((x0 || ['f,b']) | (divset ((R . r),k))))) * (vol (divset ((R . r),k))) is V11() real ext-real Element of REAL
x . k is V11() real ext-real Element of REAL
len (lower_volume ((x0 || ['a,b']),(N . r))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real positive non negative V45() V46() V47() V48() V49() V50() V58() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom (lower_volume ((x0 || ['a,b']),(N . r))) is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
k is epsilon-transitive epsilon-connected ordinal natural V11() real integer ext-real non negative V58() V63() set
dom m is V45() V46() V47() V48() V49() V50() V58() bounded_below bounded_above real-bounded Element of K6(NAT)
Seg (len m) is V45() V46() V47() V48() V49() V50() V58() V65( len m) bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len m ) } is set
Seg (len S1) is non empty V45() V46() V47() V48() V49() V50() V58() V65( len S1) left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= len S1 ) } is set
dom S1 is non empty V45() V46() V47() V48() V49() V50() V58() left_end right_end bounded_below bounded_above real-bounded Element of K6(NAT)
dom n is V45() V46() V47() V48() V49() V50() V58() bounded_below bounded_above real-bounded Element of K6(NAT)
n . k is V11() real ext-real Element of REAL
divset ((N . r),k) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
(x0 || ['a,b']) | (divset ((N . r),k)) is Relation-like ['a,b'] -defined divset ((N . r),k) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
rng ((x0 || ['a,b']) | (divset ((N . r),k))) is V45() V46() V47() Element of K6(REAL)
lower_bound (rng ((x0 || ['a,b']) | (divset ((N . r),k)))) is V11() real ext-real Element of REAL
vol (divset ((N . r),k)) is V11() real ext-real Element of REAL
upper_bound (divset ((N . r),k)) is V11() real ext-real Element of REAL
lower_bound (divset ((N . r),k)) is V11() real ext-real Element of REAL
(upper_bound (divset ((N . r),k))) - (lower_bound (divset ((N . r),k))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((N . r),k))) is V11() real ext-real set
(upper_bound (divset ((N . r),k))) + (- (lower_bound (divset ((N . r),k)))) is V11() real ext-real set
(lower_bound (rng ((x0 || ['a,b']) | (divset ((N . r),k))))) * (vol (divset ((N . r),k))) is V11() real ext-real Element of REAL
divset ((p . r),k) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
(x0 || ['a,f']) | (divset ((p . r),k)) is Relation-like ['a,f'] -defined divset ((p . r),k) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,f'],REAL))
rng ((x0 || ['a,f']) | (divset ((p . r),k))) is V45() V46() V47() Element of K6(REAL)
lower_bound (rng ((x0 || ['a,f']) | (divset ((p . r),k)))) is V11() real ext-real Element of REAL
vol (divset ((p . r),k)) is V11() real ext-real Element of REAL
upper_bound (divset ((p . r),k)) is V11() real ext-real Element of REAL
lower_bound (divset ((p . r),k)) is V11() real ext-real Element of REAL
(upper_bound (divset ((p . r),k))) - (lower_bound (divset ((p . r),k))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((p . r),k))) is V11() real ext-real set
(upper_bound (divset ((p . r),k))) + (- (lower_bound (divset ((p . r),k)))) is V11() real ext-real set
(lower_bound (rng ((x0 || ['a,f']) | (divset ((p . r),k))))) * (vol (divset ((p . r),k))) is V11() real ext-real Element of REAL
m . k is V11() real ext-real Element of REAL
Seg ((len m) + (len x)) is V45() V46() V47() V48() V49() V50() V58() V65((len m) + (len x)) bounded_below bounded_above real-bounded Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT : ( 1 <= b₁ & b₁ <= (len m) + (len x) ) } is set
r is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
N . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,b']
lower_volume ((x0 || ['a,b']),(N . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (lower_volume ((x0 || ['a,b']),(N . r))) is V11() real ext-real Element of REAL
p . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
lower_volume ((x0 || ['a,f']),(p . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (lower_volume ((x0 || ['a,f']),(p . r))) is V11() real ext-real Element of REAL
R . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
lower_volume ((x0 || ['f,b']),(R . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (lower_volume ((x0 || ['f,b']),(R . r))) is V11() real ext-real Element of REAL
(Sum (lower_volume ((x0 || ['a,f']),(p . r)))) + (Sum (lower_volume ((x0 || ['f,b']),(R . r)))) is V11() real ext-real Element of REAL
(lower_volume ((x0 || ['a,f']),(p . r))) ^ (lower_volume ((x0 || ['f,b']),(R . r))) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
lower_sum ((x0 || ['a,b']),N) 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))
r is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
(lower_sum ((x0 || ['a,b']),N)) . r is V11() real ext-real Element of REAL
N . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,b']
lower_sum ((x0 || ['a,b']),(N . r)) is V11() real ext-real Element of REAL
lower_volume ((x0 || ['a,b']),(N . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (lower_volume ((x0 || ['a,b']),(N . r))) is V11() real ext-real Element of REAL
p . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['a,f']
lower_sum ((x0 || ['a,f']),(p . r)) is V11() real ext-real Element of REAL
lower_volume ((x0 || ['a,f']),(p . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (lower_volume ((x0 || ['a,f']),(p . r))) is V11() real ext-real Element of REAL
R . r is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued increasing non-decreasing V58() FinSequence-like FinSubsequence-like Division of ['f,b']
lower_volume ((x0 || ['f,b']),(R . r)) is non empty Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V58() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (lower_volume ((x0 || ['f,b']),(R . r))) is V11() real ext-real Element of REAL
(lower_sum ((x0 || ['a,f']),(p . r))) + (Sum (lower_volume ((x0 || ['f,b']),(R . r)))) is V11() real ext-real Element of REAL
lower_sum ((x0 || ['a,f']),p) 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))
(lower_sum ((x0 || ['a,f']),p)) . r is V11() real ext-real Element of REAL
lower_sum ((x0 || ['f,b']),(R . r)) is V11() real ext-real Element of REAL
((lower_sum ((x0 || ['a,f']),p)) . r) + (lower_sum ((x0 || ['f,b']),(R . r))) is V11() real ext-real Element of REAL
lower_sum ((x0 || ['f,b']),R) 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))
(lower_sum ((x0 || ['f,b']),R)) . r is V11() real ext-real Element of REAL
((lower_sum ((x0 || ['a,f']),p)) . r) + ((lower_sum ((x0 || ['f,b']),R)) . r) is V11() real ext-real Element of REAL
(lower_sum ((x0 || ['a,f']),p)) + (lower_sum ((x0 || ['f,b']),R)) 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))
lim (upper_sum ((x0 || ['a,f']),p)) is V11() real ext-real Element of REAL
(upper_integral (x0 || ['a,f'])) + (upper_integral (x0 || ['f,b'])) is V11() real ext-real Element of REAL
lim (lower_sum ((x0 || ['a,f']),p)) is V11() real ext-real Element of REAL
lower_integral (x0 || ['a,f']) is V11() real ext-real Element of REAL
lower_sum_set (x0 || ['a,f']) is non empty Relation-like divs ['a,f'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,f']),REAL))
rng (lower_sum_set (x0 || ['a,f'])) is non empty V45() V46() V47() Element of K6(REAL)
upper_bound (rng (lower_sum_set (x0 || ['a,f']))) is V11() real ext-real Element of REAL
lower_integral (x0 || ['a,b']) is V11() real ext-real Element of REAL
lower_sum_set (x0 || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
rng (lower_sum_set (x0 || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
upper_bound (rng (lower_sum_set (x0 || ['a,b']))) is V11() real ext-real Element of REAL
lim (lower_sum ((x0 || ['a,b']),N)) is V11() real ext-real Element of REAL
lim (lower_sum ((x0 || ['f,b']),R)) is V11() real ext-real Element of REAL
(lower_integral (x0 || ['a,f'])) + (lower_integral (x0 || ['f,b'])) is V11() real ext-real Element of REAL
integral (x0,['a,b']) is V11() real ext-real Element of REAL
integral (x0 || ['a,b']) is V11() real ext-real Element of REAL
(integral (x0 || ['a,f'])) + (integral (x0 || ['f,b'])) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is V11() real ext-real set
['a,f'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
['f,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
x0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
x0 | ['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 x0 is set
integral (x0,a,b) is V11() real ext-real Element of REAL
integral (x0,a,f) is V11() real ext-real Element of REAL
integral (x0,f,b) is V11() real ext-real Element of REAL
(integral (x0,a,f)) + (integral (x0,f,b)) is V11() real ext-real Element of REAL
[.f,b.] is V45() V46() V47() closed interval Element of K6(REAL)
lower_bound ['f,b'] is V11() real ext-real Element of REAL
upper_bound ['f,b'] is V11() real ext-real Element of REAL
[.(lower_bound ['f,b']),(upper_bound ['f,b']).] is V45() V46() V47() closed interval Element of K6(REAL)
vol ['f,b'] is V11() real ext-real Element of REAL
(upper_bound ['f,b']) - (lower_bound ['f,b']) is V11() real ext-real Element of REAL
- (lower_bound ['f,b']) is V11() real ext-real set
(upper_bound ['f,b']) + (- (lower_bound ['f,b'])) is V11() real ext-real set
x0 || ['f,b'] is Relation-like ['f,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['f,b'],REAL))
K7(['f,b'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['f,b'],REAL)) is V2() V58() set
integral (x0,['f,b']) is V11() real ext-real Element of REAL
integral (x0 || ['f,b']) is V11() real ext-real Element of REAL
upper_integral (x0 || ['f,b']) is V11() real ext-real Element of REAL
upper_sum_set (x0 || ['f,b']) is non empty Relation-like divs ['f,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['f,b']),REAL))
divs ['f,b'] is non empty set
K7((divs ['f,b']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['f,b']),REAL)) is V2() V58() set
rng (upper_sum_set (x0 || ['f,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (x0 || ['f,b']))) is V11() real ext-real Element of REAL
a is V11() real ext-real set
f is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
['a,f'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
['f,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
[.a,b.] is V45() V46() V47() closed interval Element of K6(REAL)
[.f,b.] is V45() V46() V47() closed interval Element of K6(REAL)
[.a,f.] is V45() V46() V47() closed interval Element of K6(REAL)
a is V11() real ext-real set
b is V11() real ext-real set
f is V11() real ext-real set
['b,f'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
x0 is V11() real ext-real set
['a,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval 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 | ['a,x0'] is Relation-like REAL -defined ['a,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom F is set
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))
['b,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(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
f is V11() real ext-real set
['b,f'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
x0 is V11() real ext-real set
['a,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval 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 | ['a,x0'] is Relation-like REAL -defined ['a,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom F is set
c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
c₆ | ['a,x0'] is Relation-like REAL -defined ['a,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom c₆ is set
F + c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(F + c₆) | ['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))
['b,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
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))
c₆ | ['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))
['b,f'] /\ ['b,f'] is V45() V46() V47() interval Element of K6(REAL)
(F + c₆) | (['b,f'] /\ ['b,f']) is Relation-like REAL -defined ['b,f'] /\ ['b,f'] -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
f is V11() real ext-real set
x0 is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval 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 | ['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 set
integral (F,a,x0) is V11() real ext-real Element of REAL
integral (F,a,f) is V11() real ext-real Element of REAL
integral (F,f,x0) is V11() real ext-real Element of REAL
(integral (F,a,f)) + (integral (F,f,x0)) is V11() real ext-real Element of REAL
['a,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
[.a,b.] is V45() V46() V47() closed interval Element of K6(REAL)
F | ['a,x0'] is Relation-like REAL -defined ['a,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
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is V11() real ext-real set
x0 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,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 set
integral (F,a,x0) is V11() real ext-real Element of REAL
integral (F,a,f) is V11() real ext-real Element of REAL
integral (F,f,x0) is V11() real ext-real Element of REAL
(integral (F,a,f)) + (integral (F,f,x0)) is V11() real ext-real Element of REAL
integral (F,x0,f) is V11() real ext-real Element of REAL
(integral (F,a,x0)) + (integral (F,x0,f)) is V11() real ext-real Element of REAL
(integral (F,a,f)) - (integral (F,x0,f)) is V11() real ext-real Element of REAL
- (integral (F,x0,f)) is V11() real ext-real set
(integral (F,a,f)) + (- (integral (F,x0,f))) is V11() real ext-real set
['x0,f'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
integral (F,['x0,f']) is V11() real ext-real Element of REAL
F || ['x0,f'] is Relation-like ['x0,f'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['x0,f'],REAL))
K7(['x0,f'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['x0,f'],REAL)) is V2() V58() set
integral (F || ['x0,f']) is V11() real ext-real Element of REAL
upper_integral (F || ['x0,f']) is V11() real ext-real Element of REAL
upper_sum_set (F || ['x0,f']) is non empty Relation-like divs ['x0,f'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['x0,f']),REAL))
divs ['x0,f'] is non empty set
K7((divs ['x0,f']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['x0,f']),REAL)) is V2() V58() set
rng (upper_sum_set (F || ['x0,f'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (F || ['x0,f']))) is V11() real ext-real Element of REAL
- (integral (F,['x0,f'])) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
f is V11() real ext-real set
x0 is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
['f,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval 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 | ['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 set
abs F is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (abs F) is set
(abs F) | ['f,x0'] is Relation-like REAL -defined ['f,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral (F,f,x0) is V11() real ext-real Element of REAL
abs (integral (F,f,x0)) is V11() real ext-real Element of REAL
integral ((abs F),f,x0) is V11() real ext-real Element of REAL
[.a,b.] is V45() V46() V47() closed interval Element of K6(REAL)
F | ['f,x0'] is Relation-like REAL -defined ['f,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
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is V11() real ext-real set
x0 is V11() real ext-real set
min (f,x0) is V11() real ext-real set
max (f,x0) is V11() real ext-real set
['(min (f,x0)),(max (f,x0))'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval 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 | ['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 set
abs F is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (abs F) is set
(abs F) | ['(min (f,x0)),(max (f,x0))'] is Relation-like REAL -defined ['(min (f,x0)),(max (f,x0))'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral (F,f,x0) is V11() real ext-real Element of REAL
abs (integral (F,f,x0)) is V11() real ext-real Element of REAL
integral ((abs F),(min (f,x0)),(max (f,x0))) is V11() real ext-real Element of REAL
['x0,f'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
integral (F,['x0,f']) is V11() real ext-real Element of REAL
F || ['x0,f'] is Relation-like ['x0,f'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['x0,f'],REAL))
K7(['x0,f'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['x0,f'],REAL)) is V2() V58() set
integral (F || ['x0,f']) is V11() real ext-real Element of REAL
upper_integral (F || ['x0,f']) is V11() real ext-real Element of REAL
upper_sum_set (F || ['x0,f']) is non empty Relation-like divs ['x0,f'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['x0,f']),REAL))
divs ['x0,f'] is non empty set
K7((divs ['x0,f']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['x0,f']),REAL)) is V2() V58() set
rng (upper_sum_set (F || ['x0,f'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (F || ['x0,f']))) is V11() real ext-real Element of REAL
- (integral (F,['x0,f'])) is V11() real ext-real Element of REAL
integral (F,x0,f) is V11() real ext-real Element of REAL
- (integral (F,x0,f)) is V11() real ext-real Element of REAL
abs (integral (F,x0,f)) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is V11() real ext-real set
x0 is V11() real ext-real set
['f,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval 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 | ['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 set
abs F is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (abs F) is set
(abs F) | ['f,x0'] is Relation-like REAL -defined ['f,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral (F,f,x0) is V11() real ext-real Element of REAL
abs (integral (F,f,x0)) is V11() real ext-real Element of REAL
integral ((abs F),f,x0) is V11() real ext-real Element of REAL
min (f,x0) is V11() real ext-real set
max (f,x0) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is V11() real ext-real set
x0 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,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 set
integral (F,x0,f) is V11() real ext-real Element of REAL
abs (integral (F,x0,f)) 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 Element of K6(K7(REAL,REAL))
integral ((abs F),f,x0) is V11() real ext-real Element of REAL
integral (F,f,x0) is V11() real ext-real Element of REAL
abs (integral (F,f,x0)) is V11() real ext-real Element of REAL
['f,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
integral (F,['f,x0']) is V11() real ext-real Element of REAL
F || ['f,x0'] is Relation-like ['f,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['f,x0'],REAL))
K7(['f,x0'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['f,x0'],REAL)) is V2() V58() set
integral (F || ['f,x0']) is V11() real ext-real Element of REAL
upper_integral (F || ['f,x0']) is V11() real ext-real Element of REAL
upper_sum_set (F || ['f,x0']) is non empty Relation-like divs ['f,x0'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['f,x0']),REAL))
divs ['f,x0'] is non empty set
K7((divs ['f,x0']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['f,x0']),REAL)) is V2() V58() set
rng (upper_sum_set (F || ['f,x0'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (F || ['f,x0']))) is V11() real ext-real Element of REAL
- (integral (F,['f,x0'])) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
f is V11() real ext-real set
x0 is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval 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 | ['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 set
['f,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
abs F is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (abs F) is set
(abs F) | ['f,x0'] is Relation-like REAL -defined ['f,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral (F,f,x0) is V11() real ext-real Element of REAL
abs (integral (F,f,x0)) is V11() real ext-real Element of REAL
integral ((abs F),f,x0) is V11() real ext-real Element of REAL
integral (F,x0,f) is V11() real ext-real Element of REAL
abs (integral (F,x0,f)) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is V11() real ext-real set
x0 is V11() real ext-real set
min (f,x0) is V11() real ext-real set
max (f,x0) is V11() real ext-real set
['(min (f,x0)),(max (f,x0))'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
x0 - f is V11() real ext-real set
- f is V11() real ext-real set
x0 + (- f) is V11() real ext-real set
abs (x0 - f) is V11() real ext-real Element of REAL
F is V11() real ext-real set
F * (abs (x0 - f)) is V11() real ext-real Element of REAL
c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
c₆ | ['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 c₆ is set
integral (c₆,f,x0) is V11() real ext-real Element of REAL
abs (integral (c₆,f,x0)) is V11() real ext-real Element of REAL
abs c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
rng (abs c₆) is V45() V46() V47() Element of K6(REAL)
dom (abs c₆) is set
K7((dom (abs c₆)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7((dom (abs c₆)),REAL)) is set
K7(['(min (f,x0)),(max (f,x0))'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['(min (f,x0)),(max (f,x0))'],REAL)) is V2() V58() set
(abs c₆) || ['(min (f,x0)),(max (f,x0))'] is Relation-like ['(min (f,x0)),(max (f,x0))'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['(min (f,x0)),(max (f,x0))'],REAL))
vol ['(min (f,x0)),(max (f,x0))'] is V11() real ext-real Element of REAL
upper_bound ['(min (f,x0)),(max (f,x0))'] is V11() real ext-real Element of REAL
lower_bound ['(min (f,x0)),(max (f,x0))'] is V11() real ext-real Element of REAL
(upper_bound ['(min (f,x0)),(max (f,x0))']) - (lower_bound ['(min (f,x0)),(max (f,x0))']) is V11() real ext-real Element of REAL
- (lower_bound ['(min (f,x0)),(max (f,x0))']) is V11() real ext-real set
(upper_bound ['(min (f,x0)),(max (f,x0))']) + (- (lower_bound ['(min (f,x0)),(max (f,x0))'])) is V11() real ext-real set
L is non empty Relation-like ['(min (f,x0)),(max (f,x0))'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(['(min (f,x0)),(max (f,x0))'],REAL))
R is V11() real ext-real Element of REAL
{R} is non empty V2() V45() V46() V47() V58() V65(1) left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
R is non empty Relation-like ['(min (f,x0)),(max (f,x0))'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(['(min (f,x0)),(max (f,x0))'],REAL))
rng R is non empty V45() V46() V47() Element of K6(REAL)
R | ['(min (f,x0)),(max (f,x0))'] is Relation-like ['(min (f,x0)),(max (f,x0))'] -defined ['(min (f,x0)),(max (f,x0))'] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['(min (f,x0)),(max (f,x0))'],REAL))
N is V11() real ext-real Element of REAL
L . N is V11() real ext-real Element of REAL
(abs c₆) . N is V11() real ext-real Element of REAL
c₆ . N is V11() real ext-real Element of REAL
abs (c₆ . N) is V11() real ext-real Element of REAL
R . N is V11() real ext-real Element of REAL
integral ((abs c₆),(min (f,x0)),(max (f,x0))) is V11() real ext-real Element of REAL
integral ((abs c₆),['(min (f,x0)),(max (f,x0))']) is V11() real ext-real Element of REAL
integral ((abs c₆) || ['(min (f,x0)),(max (f,x0))']) is V11() real ext-real Element of REAL
upper_integral ((abs c₆) || ['(min (f,x0)),(max (f,x0))']) is V11() real ext-real Element of REAL
upper_sum_set ((abs c₆) || ['(min (f,x0)),(max (f,x0))']) is non empty Relation-like divs ['(min (f,x0)),(max (f,x0))'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['(min (f,x0)),(max (f,x0))']),REAL))
divs ['(min (f,x0)),(max (f,x0))'] is non empty set
K7((divs ['(min (f,x0)),(max (f,x0))']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['(min (f,x0)),(max (f,x0))']),REAL)) is V2() V58() set
rng (upper_sum_set ((abs c₆) || ['(min (f,x0)),(max (f,x0))'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((abs c₆) || ['(min (f,x0)),(max (f,x0))']))) is V11() real ext-real Element of REAL
(abs c₆) | ['(min (f,x0)),(max (f,x0))'] is Relation-like REAL -defined ['(min (f,x0)),(max (f,x0))'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
L | ['(min (f,x0)),(max (f,x0))'] is Relation-like ['(min (f,x0)),(max (f,x0))'] -defined ['(min (f,x0)),(max (f,x0))'] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['(min (f,x0)),(max (f,x0))'],REAL))
integral R is V11() real ext-real Element of REAL
upper_integral R is V11() real ext-real Element of REAL
upper_sum_set R is non empty Relation-like divs ['(min (f,x0)),(max (f,x0))'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['(min (f,x0)),(max (f,x0))']),REAL))
rng (upper_sum_set R) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set R)) is V11() real ext-real Element of REAL
R * (vol ['(min (f,x0)),(max (f,x0))']) is V11() real ext-real Element of REAL
R * (abs (x0 - f)) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is V11() real ext-real set
x0 is V11() real ext-real set
['f,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
x0 - f is V11() real ext-real set
- f is V11() real ext-real set
x0 + (- f) is V11() real ext-real set
F is V11() real ext-real set
F * (x0 - f) is V11() real ext-real set
c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
c₆ | ['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 c₆ is set
integral (c₆,f,x0) is V11() real ext-real Element of REAL
abs (integral (c₆,f,x0)) is V11() real ext-real Element of REAL
abs (x0 - f) is V11() real ext-real Element of REAL
min (f,x0) is V11() real ext-real set
max (f,x0) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is V11() real ext-real set
x0 is V11() real ext-real set
['f,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
x0 - f is V11() real ext-real set
- f is V11() real ext-real set
x0 + (- f) is V11() real ext-real set
F is V11() real ext-real set
F * (x0 - f) is V11() real ext-real set
c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
c₆ | ['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 c₆ is set
integral (c₆,x0,f) is V11() real ext-real Element of REAL
abs (integral (c₆,x0,f)) is V11() real ext-real Element of REAL
integral (c₆,f,x0) is V11() real ext-real Element of REAL
abs (integral (c₆,f,x0)) is V11() real ext-real Element of REAL
integral (c₆,['f,x0']) is V11() real ext-real Element of REAL
c₆ || ['f,x0'] is Relation-like ['f,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['f,x0'],REAL))
K7(['f,x0'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['f,x0'],REAL)) is V2() V58() set
integral (c₆ || ['f,x0']) is V11() real ext-real Element of REAL
upper_integral (c₆ || ['f,x0']) is V11() real ext-real Element of REAL
upper_sum_set (c₆ || ['f,x0']) is non empty Relation-like divs ['f,x0'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['f,x0']),REAL))
divs ['f,x0'] is non empty set
K7((divs ['f,x0']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['f,x0']),REAL)) is V2() V58() set
rng (upper_sum_set (c₆ || ['f,x0'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (c₆ || ['f,x0']))) is V11() real ext-real Element of REAL
- (integral (c₆,['f,x0'])) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
f is V11() real ext-real set
x0 is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
c₆ | ['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 c₆ is set
['f,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
F is V11() real ext-real set
integral (c₆,f,x0) is V11() real ext-real Element of REAL
abs (integral (c₆,f,x0)) is V11() real ext-real Element of REAL
x0 - f is V11() real ext-real set
- f is V11() real ext-real set
x0 + (- f) is V11() real ext-real set
F * (x0 - f) is V11() real ext-real set
integral (c₆,x0,f) is V11() real ext-real Element of REAL
abs (integral (c₆,x0,f)) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
f is V11() real ext-real set
x0 is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
['f,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval 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))
c₆ 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))
c₆ | ['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 set
dom c₆ is set
F + c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(F + c₆) | ['f,x0'] is Relation-like REAL -defined ['f,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((F + c₆),f,x0) is V11() real ext-real Element of REAL
integral (F,f,x0) is V11() real ext-real Element of REAL
integral (c₆,f,x0) is V11() real ext-real Element of REAL
(integral (F,f,x0)) + (integral (c₆,f,x0)) is V11() real ext-real Element of REAL
F - c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
(F - c₆) | ['f,x0'] is Relation-like REAL -defined ['f,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((F - c₆),f,x0) is V11() real ext-real Element of REAL
(integral (F,f,x0)) - (integral (c₆,f,x0)) is V11() real ext-real Element of REAL
- (integral (c₆,f,x0)) is V11() real ext-real set
(integral (F,f,x0)) + (- (integral (c₆,f,x0))) is V11() real ext-real set
[.a,b.] is V45() V46() V47() closed interval Element of K6(REAL)
F | ['f,x0'] is Relation-like REAL -defined ['f,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
c₆ | ['f,x0'] is Relation-like REAL -defined ['f,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
['f,x0'] /\ ['f,x0'] is V45() V46() V47() interval Element of K6(REAL)
(F + c₆) | (['f,x0'] /\ ['f,x0']) is Relation-like REAL -defined ['f,x0'] /\ ['f,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
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is V11() real ext-real set
x0 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,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 set
integral (F,f,x0) is V11() real ext-real Element of REAL
c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
c₆ | ['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 c₆ is set
F + c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((F + c₆),f,x0) is V11() real ext-real Element of REAL
integral (c₆,f,x0) is V11() real ext-real Element of REAL
(integral (F,f,x0)) + (integral (c₆,f,x0)) is V11() real ext-real Element of REAL
F - c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((F - c₆),f,x0) is V11() real ext-real Element of REAL
(integral (F,f,x0)) - (integral (c₆,f,x0)) is V11() real ext-real Element of REAL
- (integral (c₆,f,x0)) is V11() real ext-real set
(integral (F,f,x0)) + (- (integral (c₆,f,x0))) is V11() real ext-real set
['x0,f'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
integral (F,['x0,f']) is V11() real ext-real Element of REAL
F || ['x0,f'] is Relation-like ['x0,f'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['x0,f'],REAL))
K7(['x0,f'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['x0,f'],REAL)) is V2() V58() set
integral (F || ['x0,f']) is V11() real ext-real Element of REAL
upper_integral (F || ['x0,f']) is V11() real ext-real Element of REAL
upper_sum_set (F || ['x0,f']) is non empty Relation-like divs ['x0,f'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['x0,f']),REAL))
divs ['x0,f'] is non empty set
K7((divs ['x0,f']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['x0,f']),REAL)) is V2() V58() set
rng (upper_sum_set (F || ['x0,f'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (F || ['x0,f']))) is V11() real ext-real Element of REAL
- (integral (F,['x0,f'])) is V11() real ext-real Element of REAL
integral (c₆,['x0,f']) is V11() real ext-real Element of REAL
c₆ || ['x0,f'] is Relation-like ['x0,f'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['x0,f'],REAL))
integral (c₆ || ['x0,f']) is V11() real ext-real Element of REAL
upper_integral (c₆ || ['x0,f']) is V11() real ext-real Element of REAL
upper_sum_set (c₆ || ['x0,f']) is non empty Relation-like divs ['x0,f'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['x0,f']),REAL))
rng (upper_sum_set (c₆ || ['x0,f'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (c₆ || ['x0,f']))) is V11() real ext-real Element of REAL
- (integral (c₆,['x0,f'])) is V11() real ext-real Element of REAL
integral ((F + c₆),['x0,f']) is V11() real ext-real Element of REAL
(F + c₆) || ['x0,f'] is Relation-like ['x0,f'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['x0,f'],REAL))
integral ((F + c₆) || ['x0,f']) is V11() real ext-real Element of REAL
upper_integral ((F + c₆) || ['x0,f']) is V11() real ext-real Element of REAL
upper_sum_set ((F + c₆) || ['x0,f']) is non empty Relation-like divs ['x0,f'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['x0,f']),REAL))
rng (upper_sum_set ((F + c₆) || ['x0,f'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((F + c₆) || ['x0,f']))) is V11() real ext-real Element of REAL
- (integral ((F + c₆),['x0,f'])) is V11() real ext-real Element of REAL
integral ((F + c₆),x0,f) is V11() real ext-real Element of REAL
- (integral ((F + c₆),x0,f)) is V11() real ext-real Element of REAL
integral (F,x0,f) is V11() real ext-real Element of REAL
integral (c₆,x0,f) is V11() real ext-real Element of REAL
(integral (F,x0,f)) + (integral (c₆,x0,f)) is V11() real ext-real Element of REAL
- ((integral (F,x0,f)) + (integral (c₆,x0,f))) is V11() real ext-real Element of REAL
- (integral (F,x0,f)) is V11() real ext-real Element of REAL
(- (integral (F,x0,f))) - (integral (c₆,x0,f)) is V11() real ext-real Element of REAL
- (integral (c₆,x0,f)) is V11() real ext-real set
(- (integral (F,x0,f))) + (- (integral (c₆,x0,f))) is V11() real ext-real set
(integral (F,f,x0)) - (integral (c₆,x0,f)) is V11() real ext-real Element of REAL
(integral (F,f,x0)) + (- (integral (c₆,x0,f))) is V11() real ext-real set
integral ((F - c₆),['x0,f']) is V11() real ext-real Element of REAL
(F - c₆) || ['x0,f'] is Relation-like ['x0,f'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['x0,f'],REAL))
integral ((F - c₆) || ['x0,f']) is V11() real ext-real Element of REAL
upper_integral ((F - c₆) || ['x0,f']) is V11() real ext-real Element of REAL
upper_sum_set ((F - c₆) || ['x0,f']) is non empty Relation-like divs ['x0,f'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['x0,f']),REAL))
rng (upper_sum_set ((F - c₆) || ['x0,f'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((F - c₆) || ['x0,f']))) is V11() real ext-real Element of REAL
- (integral ((F - c₆),['x0,f'])) is V11() real ext-real Element of REAL
integral ((F - c₆),x0,f) is V11() real ext-real Element of REAL
- (integral ((F - c₆),x0,f)) is V11() real ext-real Element of REAL
(integral (F,x0,f)) - (integral (c₆,x0,f)) is V11() real ext-real Element of REAL
(integral (F,x0,f)) + (- (integral (c₆,x0,f))) is V11() real ext-real set
- ((integral (F,x0,f)) - (integral (c₆,x0,f))) is V11() real ext-real Element of REAL
(integral (F,x0,f)) + (integral (c₆,f,x0)) is V11() real ext-real Element of REAL
- ((integral (F,x0,f)) + (integral (c₆,f,x0))) is V11() real ext-real Element of REAL
(- (integral (F,x0,f))) - (integral (c₆,f,x0)) is V11() real ext-real Element of REAL
(- (integral (F,x0,f))) + (- (integral (c₆,f,x0))) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
f is V11() real ext-real set
x0 is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
F is V11() real ext-real set
c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
c₆ | ['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 c₆ is set
F (#) c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((F (#) c₆),f,x0) is V11() real ext-real Element of REAL
integral (c₆,f,x0) is V11() real ext-real Element of REAL
F * (integral (c₆,f,x0)) is V11() real ext-real Element of REAL
[.a,b.] is V45() V46() V47() closed interval Element of K6(REAL)
['f,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
c₆ | ['f,x0'] is Relation-like REAL -defined ['f,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
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is V11() real ext-real set
x0 is V11() real ext-real set
F is V11() real ext-real set
c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
c₆ | ['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 c₆ is set
F (#) c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
integral ((F (#) c₆),f,x0) is V11() real ext-real Element of REAL
integral (c₆,f,x0) is V11() real ext-real Element of REAL
F * (integral (c₆,f,x0)) is V11() real ext-real Element of REAL
['x0,f'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
integral (c₆,['x0,f']) is V11() real ext-real Element of REAL
c₆ || ['x0,f'] is Relation-like ['x0,f'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['x0,f'],REAL))
K7(['x0,f'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['x0,f'],REAL)) is V2() V58() set
integral (c₆ || ['x0,f']) is V11() real ext-real Element of REAL
upper_integral (c₆ || ['x0,f']) is V11() real ext-real Element of REAL
upper_sum_set (c₆ || ['x0,f']) is non empty Relation-like divs ['x0,f'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['x0,f']),REAL))
divs ['x0,f'] is non empty set
K7((divs ['x0,f']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['x0,f']),REAL)) is V2() V58() set
rng (upper_sum_set (c₆ || ['x0,f'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (c₆ || ['x0,f']))) is V11() real ext-real Element of REAL
- (integral (c₆,['x0,f'])) is V11() real ext-real Element of REAL
integral ((F (#) c₆),['x0,f']) is V11() real ext-real Element of REAL
(F (#) c₆) || ['x0,f'] is Relation-like ['x0,f'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['x0,f'],REAL))
integral ((F (#) c₆) || ['x0,f']) is V11() real ext-real Element of REAL
upper_integral ((F (#) c₆) || ['x0,f']) is V11() real ext-real Element of REAL
upper_sum_set ((F (#) c₆) || ['x0,f']) is non empty Relation-like divs ['x0,f'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['x0,f']),REAL))
rng (upper_sum_set ((F (#) c₆) || ['x0,f'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((F (#) c₆) || ['x0,f']))) is V11() real ext-real Element of REAL
- (integral ((F (#) c₆),['x0,f'])) is V11() real ext-real Element of REAL
integral ((F (#) c₆),x0,f) is V11() real ext-real Element of REAL
- (integral ((F (#) c₆),x0,f)) is V11() real ext-real Element of REAL
integral (c₆,x0,f) is V11() real ext-real Element of REAL
F * (integral (c₆,x0,f)) is V11() real ext-real Element of REAL
- (F * (integral (c₆,x0,f))) is V11() real ext-real Element of REAL
- (integral (c₆,x0,f)) is V11() real ext-real Element of REAL
F * (- (integral (c₆,x0,f))) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
b - a is V11() real ext-real set
- a is V11() real ext-real set
b + (- a) is V11() real ext-real set
f is V11() real ext-real set
f * (b - a) is V11() real ext-real set
x0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom x0 is set
x0 | ['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))
integral (x0,a,b) is V11() real ext-real Element of REAL
rng x0 is V45() V46() V47() Element of K6(REAL)
K7((dom x0),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K6(K7((dom x0),REAL)) is set
K7(['a,b'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['a,b'],REAL)) is V2() V58() set
x0 || ['a,b'] is Relation-like ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
c₆ is V11() real ext-real Element of REAL
{c₆} is non empty V2() V45() V46() V47() V58() V65(1) left_end right_end bounded_below bounded_above real-bounded Element of K6(REAL)
x is non empty Relation-like ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
rng x is non empty V45() V46() V47() Element of K6(REAL)
x | ['a,b'] is Relation-like ['a,b'] -defined ['a,b'] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
integral x is V11() real ext-real Element of REAL
upper_integral x is V11() real ext-real Element of REAL
upper_sum_set x is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
divs ['a,b'] is non empty set
K7((divs ['a,b']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['a,b']),REAL)) is V2() V58() set
rng (upper_sum_set x) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set x)) is V11() real ext-real Element of REAL
vol ['a,b'] is V11() real ext-real Element of REAL
upper_bound ['a,b'] is V11() real ext-real Element of REAL
lower_bound ['a,b'] is V11() real ext-real Element of REAL
(upper_bound ['a,b']) - (lower_bound ['a,b']) is V11() real ext-real Element of REAL
- (lower_bound ['a,b']) is V11() real ext-real set
(upper_bound ['a,b']) + (- (lower_bound ['a,b'])) is V11() real ext-real set
c₆ * (vol ['a,b']) is V11() real ext-real Element of REAL
F is non empty Relation-like ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7(['a,b'],REAL))
L is set
F . L is V11() real ext-real Element of REAL
x . L is V11() real ext-real Element of REAL
R is V11() real ext-real set
x0 . R is V11() real ext-real Element of REAL
x . R is V11() real ext-real Element of REAL
dom F is non empty set
['a,b'] /\ (dom F) is V45() V46() V47() Element of K6(REAL)
L is V11() real ext-real set
(dom x0) /\ ['a,b'] is V45() V46() V47() Element of K6(REAL)
['a,b'] /\ ((dom x0) /\ ['a,b']) is V45() V46() V47() Element of K6(REAL)
['a,b'] /\ ['a,b'] is V45() V46() V47() interval Element of K6(REAL)
(['a,b'] /\ ['a,b']) /\ (dom x0) is V45() V46() V47() Element of K6(REAL)
R is set
['a,b'] /\ (dom x0) is V45() V46() V47() Element of K6(REAL)
F . R is V11() real ext-real Element of REAL
abs (F . R) is V11() real ext-real Element of REAL
x0 . R is V11() real ext-real Element of REAL
abs (x0 . R) is V11() real ext-real Element of REAL
integral (x0,['a,b']) is V11() real ext-real Element of REAL
integral (x0 || ['a,b']) is V11() real ext-real Element of REAL
upper_integral (x0 || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set (x0 || ['a,b']) is non empty Relation-like divs ['a,b'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set (x0 || ['a,b'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (x0 || ['a,b']))) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
f is V11() real ext-real set
x0 is V11() real ext-real set
F is V11() real ext-real set
F - x0 is V11() real ext-real set
- x0 is V11() real ext-real set
F + (- x0) is V11() real ext-real set
f * (F - x0) is V11() real ext-real set
c₆ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom c₆ is set
integral (c₆,x0,F) is V11() real ext-real Element of REAL
c₆ | ['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))
[.a,b.] is V45() V46() V47() closed interval Element of K6(REAL)
['x0,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
['a,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
['x0,F'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
x is V11() real ext-real set
c₆ . x is V11() real ext-real Element of REAL
['F,x0'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
x is V11() real ext-real set
c₆ . x is V11() real ext-real Element of REAL
integral (c₆,['F,x0']) is V11() real ext-real Element of REAL
c₆ || ['F,x0'] is Relation-like ['F,x0'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(['F,x0'],REAL))
K7(['F,x0'],REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7(['F,x0'],REAL)) is V2() V58() set
integral (c₆ || ['F,x0']) is V11() real ext-real Element of REAL
upper_integral (c₆ || ['F,x0']) is V11() real ext-real Element of REAL
upper_sum_set (c₆ || ['F,x0']) is non empty Relation-like divs ['F,x0'] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K6(K7((divs ['F,x0']),REAL))
divs ['F,x0'] is non empty set
K7((divs ['F,x0']),REAL) is V2() Relation-like complex-valued ext-real-valued real-valued V58() set
K6(K7((divs ['F,x0']),REAL)) is V2() V58() set
rng (upper_sum_set (c₆ || ['F,x0'])) is non empty V45() V46() V47() Element of K6(REAL)
lower_bound (rng (upper_sum_set (c₆ || ['F,x0']))) is V11() real ext-real Element of REAL
- (integral (c₆,['F,x0'])) is V11() real ext-real Element of REAL
integral (c₆,F,x0) is V11() real ext-real Element of REAL
- (integral (c₆,F,x0)) is V11() real ext-real Element of REAL
x0 - F is V11() real ext-real set
- F is V11() real ext-real set
x0 + (- F) is V11() real ext-real set
f * (x0 - F) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
].a,b.[ is V45() V46() V47() open non left_end non right_end interval 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 | ['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 set
x0 is V11() real ext-real set
f . 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))
dom F is set
diff (F,x0) is V11() real ext-real Element of REAL
c₆ 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))
F . x0 is V11() real ext-real Element of REAL
x is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
R is Relation-like Function-like set
dom R is set
rng R is set
R is set
N is set
R . N is set
R_id N is V11() real ext-real Element of REAL
x0 + (R_id N) is V11() real ext-real Element of REAL
F . (x0 + (R_id N)) is V11() real ext-real Element of REAL
(F . (x0 + (R_id N))) - (F . x0) is V11() real ext-real Element of REAL
- (F . x0) is V11() real ext-real set
(F . (x0 + (R_id N))) + (- (F . x0)) is V11() real ext-real set
x . (R_id N) is V11() real ext-real Element of REAL
((F . (x0 + (R_id N))) - (F . x0)) - (x . (R_id N)) is V11() real ext-real Element of REAL
- (x . (R_id N)) is V11() real ext-real set
((F . (x0 + (R_id N))) - (F . x0)) + (- (x . (R_id N))) is V11() real ext-real set
R is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
[.a,b.] is V45() V46() V47() closed interval Element of K6(REAL)
N 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))
N " 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))
R /* N 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))
(N ") (#) (R /* N) 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))
lim ((N ") (#) (R /* N)) is V11() real ext-real Element of REAL
REAL --> (f . x0) 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))
x is V11() real ext-real set
x / 2 is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative set
x * (2 ") is V11() real ext-real set
lim N is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued functional integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V46() V47() V48() V49() V50() V51() V58() V59() V62() V63() V65( {} ) FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval Element of REAL
p is V11() real ext-real set
p / 2 is V11() real ext-real Element of REAL
p * (2 ") is V11() real ext-real set
N is V45() V46() V47() open Neighbourhood of x0
q is V11() real ext-real set
x0 - q is V11() real ext-real set
- q is V11() real ext-real set
x0 + (- q) is V11() real ext-real set
x0 + q is V11() real ext-real set
].(x0 - q),(x0 + q).[ is V45() V46() V47() open non left_end non right_end interval Element of K6(REAL)
q / 2 is V11() real ext-real Element of REAL
q * (2 ") is V11() real ext-real set
min ((p / 2),(q / 2)) is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real integer V31() ext-real non negative V45() V46() V47() V48() V49() V50() V58() V63() bounded_below bounded_above real-bounded Element of NAT
((N ") (#) (R /* N)) . m is V11() real ext-real Element of REAL
(((N ") (#) (R /* N)) . m) - 0 is V11() real ext-real Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding RAT -valued functional integer ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V45() V46() V47() V48() V49() V50() V51() V58() V59() V62() V63() V65( {} ) FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval set
(((N ") (#) (R /* N)) . m) + (- 0) is V11() real ext-real set
abs ((((N ") (#) (R /* N)) . m) - 0) is V11() real ext-real Element of REAL
x0 - (min ((p / 2),(q / 2))) is V11() real ext-real set
- (min ((p / 2),(q / 2))) is V11() real ext-real set
x0 + (- (min ((p / 2),(q / 2)))) is V11() real ext-real set
x0 + (min ((p / 2),(q / 2))) is V11() real ext-real set
].(x0 - (min ((p / 2),(q / 2)))),(x0 + (min ((p / 2),(q / 2)))).[ is V45() V46() V47() open non left_end non right_end interval Element of K6(REAL)
N . m is V11() real ext-real Element of REAL
(N . m) - 0 is V11() real ext-real Element of REAL
(N . m) + (- 0) is V11() real ext-real set
abs ((N . m) - 0) is V11() real ext-real Element of REAL
x0 + (N . m) is V11() real ext-real Element of REAL
(x0 + (N . m)) - x0 is V11() real ext-real Element of REAL
- x0 is V11() real ext-real set
(x0 + (N . m)) + (- x0) is V11() real ext-real set
abs ((x0 + (N . m)) - x0) is V11() real ext-real Element of REAL
R_id (N . m) is V11() real ext-real Element of REAL
x0 + (R_id (N . m)) is V11() real ext-real Element of REAL
R . (N . m) is V11() real ext-real Element of REAL
F . (x0 + (R_id (N . m))) is V11() real ext-real Element of REAL
(F . (x0 + (R_id (N . m)))) - (F . x0) is V11() real ext-real Element of REAL
- (F . x0) is V11() real ext-real set
(F . (x0 + (R_id (N . m)))) + (- (F . x0)) is V11() real ext-real set
L is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
L . (R_id (N . m)) is V11() real ext-real Element of REAL
((F . (x0 + (R_id (N . m)))) - (F . x0)) - (L . (R_id (N . m))) is V11() real ext-real Element of REAL
- (L . (R_id (N . m))) is V11() real ext-real set
((F . (x0 + (R_id (N . m)))) - (F . x0)) + (- (L . (R_id (N . m)))) is V11() real ext-real set
F . (x0 + (N . m)) is V11() real ext-real Element of REAL
(F . (x0 + (N . m))) - (F . x0) is V11() real ext-real Element of REAL
(F . (x0 + (N . m))) + (- (F . x0)) is V11() real ext-real set
((F . (x0 + (N . m))) - (F . x0)) - (L . (R_id (N . m))) is V11() real ext-real Element of REAL
((F . (x0 + (N . m))) - (F . x0)) + (- (L . (R_id (N . m)))) is V11() real ext-real set
L . (N . m) is V11() real ext-real Element of REAL
((F . (x0 + (N . m))) - (F . x0)) - (L . (N . m)) is V11() real ext-real Element of REAL
- (L . (N . m)) is V11() real ext-real set
((F . (x0 + (N . m))) - (F . x0)) + (- (L . (N . m))) is V11() real ext-real set
(f . x0) * (N . m) is V11() real ext-real Element of REAL
((F . (x0 + (N . m))) - (F . x0)) - ((f . x0) * (N . m)) is V11() real ext-real Element of REAL
- ((f . x0) * (N . m)) is V11() real ext-real set
((F . (x0 + (N . m))) - (F . x0)) + (- ((f . x0) * (N . m))) is V11() real ext-real set
integral (f,a,(x0 + (N . m))) is V11() real ext-real Element of REAL
integral (f,a,x0) is V11() real ext-real Element of REAL
(integral (f,a,(x0 + (N . m)))) - (integral (f,a,x0)) is V11() real ext-real Element of REAL
- (integral (f,a,x0)) is V11() real ext-real set
(integral (f,a,(x0 + (N . m)))) + (- (integral (f,a,x0))) is V11() real ext-real set
((integral (f,a,(x0 + (N . m)))) - (integral (f,a,x0))) - ((f . x0) * (N . m)) is V11() real ext-real Element of REAL
((integral (f,a,(x0 + (N . m)))) - (integral (f,a,x0))) + (- ((f . x0) * (N . m))) is V11() real ext-real set
dom (REAL --> (f . x0)) is non empty set
['a,b'] /\ ['a,b'] is V45() V46() V47() interval Element of K6(REAL)
(dom f) /\ (dom (REAL --> (f . x0))) is set
f - (REAL --> (f . x0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
dom (f - (REAL --> (f . x0))) is set
integral (f,x0,(x0 + (N . m))) is V11() real ext-real Element of REAL
(integral (f,a,x0)) + (integral (f,x0,(x0 + (N . m)))) is V11() real ext-real Element of REAL
min (x0,(x0 + (N . m))) is V11() real ext-real set
max (x0,(x0 + (N . m))) is V11() real ext-real set
['(min (x0,(x0 + (N . m)))),(max (x0,(x0 + (N . m))))'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
x is V11() real ext-real set
(f - (REAL --> (f . x0))) . x is V11() real ext-real Element of REAL
abs ((f - (REAL --> (f . x0))) . x) is V11() real ext-real Element of REAL
[.(min (x0,(x0 + (N . m)))),(max (x0,(x0 + (N . m)))).] is V45() V46() V47() closed interval Element of K6(REAL)
x - x0 is V11() real ext-real set
x + (- x0) is V11() real ext-real set
abs (x - x0) is V11() real ext-real Element of REAL
abs (N . m) is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( x0 <= b₁ & b₁ <= x0 + (N . m) ) } is set
S1 is V11() real ext-real Element of REAL
S1 is V11() real ext-real Element of REAL
S1 is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( x0 + (N . m) <= b₁ & b₁ <= x0 ) } is set
S1 is V11() real ext-real Element of REAL
x0 - x0 is V11() real ext-real set
x0 + (- x0) is V11() real ext-real set
- (N . m) is V11() real ext-real Element of REAL
S1 is V11() real ext-real Element of REAL
- (x - x0) is V11() real ext-real set
f . x is V11() real ext-real Element of REAL
(f . x) - (f . x0) is V11() real ext-real Element of REAL
- (f . x0) is V11() real ext-real set
(f . x) + (- (f . x0)) is V11() real ext-real set
abs ((f . x) - (f . x0)) is V11() real ext-real Element of REAL
x1 is V11() real ext-real Element of REAL
f . x1 is V11() real ext-real Element of REAL
(REAL --> (f . x0)) . x1 is V11() real ext-real Element of REAL
(f . x1) - ((REAL --> (f . x0)) . x1) is V11() real ext-real Element of REAL
- ((REAL --> (f . x0)) . x1) is V11() real ext-real set
(f . x1) + (- ((REAL --> (f . x0)) . x1)) is V11() real ext-real set
abs ((f . x1) - ((REAL --> (f . x0)) . x1)) is V11() real ext-real Element of REAL
x is V11() real ext-real set
(REAL --> (f . x0)) . x is V11() real ext-real Element of REAL
(REAL --> (f . x0)) | ['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))
(f - (REAL --> (f . x0))) | (['a,b'] /\ ['a,b']) is Relation-like REAL -defined ['a,b'] /\ ['a,b'] -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))
rng N is non empty V45() V46() V47() Element of K6(REAL)
dom R is set
(R . (N . m)) / (N . m) is V11() real ext-real Element of REAL
(N . m) " is V11() real ext-real set
(R . (N . m)) * ((N . m) ") is V11() real ext-real set
(R /* N) . m is V11() real ext-real Element of REAL
((R /* N) . m) / (N . m) is V11() real ext-real Element of REAL
((R /* N) . m) * ((N . m) ") is V11() real ext-real set
(N ") . m is V11() real ext-real Element of REAL
((R /* N) . m) * ((N ") . m) is V11() real ext-real Element of REAL
abs (N . m) is V11() real ext-real Element of REAL
integral ((f - (REAL --> (f . x0))),x0,(x0 + (N . m))) is V11() real ext-real Element of REAL
abs (integral ((f - (REAL --> (f . x0))),x0,(x0 + (N . m)))) is V11() real ext-real Element of REAL
(x / 2) * (abs ((x0 + (N . m)) - x0)) is V11() real ext-real Element of REAL
integral ((REAL --> (f . x0)),x0,(x0 + (N . m))) is V11() real ext-real Element of REAL
(f . x0) * ((x0 + (N . m)) - x0) is V11() real ext-real Element of REAL
abs ((R . (N . m)) / (N . m)) is V11() real ext-real Element of REAL
abs (R . (N . m)) is V11() real ext-real Element of REAL
(abs (R . (N . m))) / (abs (N . m)) is V11() real ext-real Element of REAL
(abs (N . m)) " is V11() real ext-real set
(abs (R . (N . m))) * ((abs (N . m)) ") is V11() real ext-real set
(x / 2) * (abs (N . m)) is V11() real ext-real Element of REAL
((x / 2) * (abs (N . m))) / (abs (N . m)) is V11() real ext-real Element of REAL
((x / 2) * (abs (N . m))) * ((abs (N . m)) ") is V11() real ext-real set
N is V45() V46() V47() open Neighbourhood of x0
L is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued linear Element of K6(K7(REAL,REAL))
R is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued RestFunc-like Element of K6(K7(REAL,REAL))
x is V11() real ext-real Element of REAL
F . x is V11() real ext-real Element of REAL
(F . x) - (F . x0) is V11() real ext-real Element of REAL
- (F . x0) is V11() real ext-real set
(F . x) + (- (F . x0)) is V11() real ext-real set
x - x0 is V11() real ext-real Element of REAL
- x0 is V11() real ext-real set
x + (- x0) is V11() real ext-real set
L . (x - x0) is V11() real ext-real Element of REAL
R . (x - x0) is V11() real ext-real Element of REAL
(L . (x - x0)) + (R . (x - x0)) is V11() real ext-real Element of REAL
x0 + (x - x0) is V11() real ext-real Element of REAL
R_id (x - x0) is V11() real ext-real Element of REAL
x0 + (R_id (x - x0)) is V11() real ext-real Element of REAL
F . (x0 + (R_id (x - x0))) is V11() real ext-real Element of REAL
(F . (x0 + (R_id (x - x0)))) - (F . x0) is V11() real ext-real Element of REAL
(F . (x0 + (R_id (x - x0)))) + (- (F . x0)) is V11() real ext-real set
x . (R_id (x - x0)) is V11() real ext-real Element of REAL
((F . (x0 + (R_id (x - x0)))) - (F . x0)) - (x . (R_id (x - x0))) is V11() real ext-real Element of REAL
- (x . (R_id (x - x0))) is V11() real ext-real set
((F . (x0 + (R_id (x - x0)))) - (F . x0)) + (- (x . (R_id (x - x0)))) is V11() real ext-real set
L . 1 is V11() real ext-real Element of REAL
(f . x0) * 1 is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
].a,b.[ is V45() V46() V47() open non left_end non right_end interval 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))
x0 is Relation-like Function-like set
dom x0 is set
F is set
rng x0 is set
c₆ is set
x0 . c₆ is set
x is V11() real ext-real Element of REAL
x0 . x is set
integral (f,a,x) 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))
dom F is set
c₆ is V11() real ext-real set
F . c₆ is V11() real ext-real Element of REAL
integral (f,a,c₆) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of K6(REAL)
].a,b.[ is V45() V46() V47() open non left_end non right_end interval 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 | ['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 set
x0 is V11() real ext-real set
f . 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))
dom F is set
diff (F,x0) is V11() real ext-real Element of REAL