REAL is non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval set
NAT is non empty V12() epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() cardinal limit_cardinal left_end bounded_below Element of K19(REAL)
K19(REAL) is V12() V51() set
{} is set
RAT is non empty V12() complex-membered ext-real-membered real-membered rational-membered V50() V51() set
the Relation-like non-empty empty-yielding RAT -valued functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V34() V35() V36() V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() V52() V55() cardinal {} -element FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval set is Relation-like non-empty empty-yielding RAT -valued functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V34() V35() V36() V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() V52() V55() cardinal {} -element FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
{{},1} is V51() set
COMPLEX is non empty V12() complex-membered V50() V51() set
omega is non empty V12() epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() cardinal limit_cardinal left_end bounded_below set
K19(omega) is V12() V51() set
K19(NAT) is V12() V51() set
INT is non empty V12() complex-membered ext-real-membered real-membered rational-membered integer-membered V50() V51() set
K20(COMPLEX,COMPLEX) is Relation-like V12() V34() V51() set
K19(K20(COMPLEX,COMPLEX)) is V12() V51() set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like V12() V34() V51() set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V12() V51() set
K20(REAL,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(REAL,REAL)) is V12() V51() set
K20(K20(REAL,REAL),REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(K20(REAL,REAL),REAL)) is V12() V51() set
K20(RAT,RAT) is Relation-like RAT -valued V12() V34() V35() V36() V51() set
K19(K20(RAT,RAT)) is V12() V51() set
K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued V12() V34() V35() V36() V51() set
K19(K20(K20(RAT,RAT),RAT)) is V12() V51() set
K20(INT,INT) is Relation-like RAT -valued INT -valued V12() V34() V35() V36() V51() set
K19(K20(INT,INT)) is V12() V51() set
K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued V12() V34() V35() V36() V51() set
K19(K20(K20(INT,INT),INT)) is V12() V51() set
K20(NAT,NAT) is Relation-like RAT -valued INT -valued V12() V34() V35() V36() V37() V51() set
K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V12() V34() V35() V36() V37() V51() set
K19(K20(K20(NAT,NAT),NAT)) is V12() V51() set
K291() is set
ExtREAL is non empty ext-real-membered interval set
K20(COMPLEX,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(COMPLEX,REAL)) is V12() V51() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
card {} is epsilon-transitive epsilon-connected ordinal cardinal set
+infty is non empty non real ext-real positive non negative set
-infty is non empty non real ext-real non positive negative set
A is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
lower_bound A is V22() real ext-real Element of REAL
upper_bound A is V22() real ext-real Element of REAL
e is V22() real ext-real set
[.(lower_bound A),(upper_bound A).] is complex-membered ext-real-membered real-membered interval Element of K19(REAL)
{ b1 where b1 is V22() real ext-real Element of REAL : ( lower_bound A <= b1 & b1 <= upper_bound A ) } is set
r is V22() real ext-real Element of REAL
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V34() V35() V36() V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() V52() V55() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered bounded_below bounded_above real-bounded interval FinSequence of REAL
A is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V34() V35() V36() V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() V52() V55() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered bounded_below bounded_above real-bounded interval FinSequence of REAL
e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
dom A is Relation-like non-empty empty-yielding RAT -valued functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V34() V35() V36() V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() V52() V55() cardinal {} -element FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval Element of K19(NAT)
e + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
A . e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal Element of REAL
A . (e + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal Element of REAL
A is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like () FinSequence of REAL
dom A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)
e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
A . e is V22() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
A . r is V22() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b + (b + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
A . b is V22() real ext-real Element of REAL
c6 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
A . c6 is V22() real ext-real Element of REAL
b + b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
X + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
1 + 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
len A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
A . X is V22() real ext-real Element of REAL
c6 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b + (b + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
A . b is V22() real ext-real Element of REAL
A . c6 is V22() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b + 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
A . b is V22() real ext-real Element of REAL
A . b is V22() real ext-real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal set
e + b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
e + b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
A is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
e is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() non-increasing V51() FinSequence-like FinSubsequence-like FinSequence of REAL
Rev e is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
dom (Rev e) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)
r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
r + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
(Rev e) . r is V22() real ext-real Element of REAL
(Rev e) . (r + 1) is V22() real ext-real Element of REAL
len (Rev e) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
Seg (len (Rev e)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() len (Rev e) -element bounded_below bounded_above real-bounded Element of K19(NAT)
r - 1 is V22() real ext-real Element of REAL
len e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
(len e) + 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
(len e) + (r - 1) is V22() real ext-real Element of REAL
(len e) - (r - 1) is V22() real ext-real Element of REAL
Seg (len e) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() len e -element bounded_below bounded_above real-bounded Element of K19(NAT)
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal set
r + b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
(len e) - r is V22() real ext-real Element of REAL
((len e) - r) + 1 is V22() real ext-real Element of REAL
dom e is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)
(len e) - (r + 1) is V22() real ext-real Element of REAL
((len e) - (r + 1)) + 1 is V22() real ext-real Element of REAL
(len e) + r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
e . (((len e) - r) + 1) is V22() real ext-real Element of REAL
e . (((len e) - (r + 1)) + 1) is V22() real ext-real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like () FinSequence of REAL
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
len b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
c6 is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() non-increasing V51() FinSequence-like FinSubsequence-like FinSequence of REAL
Rev c6 is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
X is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() non-increasing V51() FinSequence-like FinSubsequence-like FinSequence of REAL
X | b is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
i is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() non-increasing V51() FinSequence-like FinSubsequence-like FinSequence of REAL
Rev i is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
X . (b + 1) is V22() real ext-real Element of REAL
<*(X . (b + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V12() V34() V35() V36() V38() V39() V40() non-increasing V51() 1 -element FinSequence-like FinSubsequence-like FinSequence of REAL
(Rev i) ^ <*(X . (b + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
<*(X . (b + 1))*> ^ (Rev i) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
len X is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
len (X | b) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
(X | b) ^ <*(X . (b + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
Rev ((X | b) ^ <*(X . (b + 1))*>) is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
Rev X is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
b is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
len b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
c6 is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() non-increasing V51() FinSequence-like FinSubsequence-like FinSequence of REAL
Rev c6 is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
len A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
len b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() non-increasing V51() FinSequence-like FinSubsequence-like FinSequence of REAL
Rev b is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
len b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
len (Rev b) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
rng (Rev b) is complex-membered ext-real-membered real-membered V51() bounded_below bounded_above real-bounded Element of K19(REAL)
rng b is complex-membered ext-real-membered real-membered V51() bounded_below bounded_above real-bounded Element of K19(REAL)
c6 is set
Coim (b,c6) is V51() set
{c6} is non empty V12() V51() 1 -element set
b " {c6} is V51() set
card (Coim (b,c6)) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of omega
Coim ((Rev b),c6) is V51() set
(Rev b) " {c6} is V51() set
card (Coim ((Rev b),c6)) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of omega
b " {c6} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)
card (b " {c6}) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of omega
A is non empty set
e is Relation-like NAT -defined A -valued Function-like V51() FinSequence-like FinSubsequence-like FinSequence of A
len e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
mid (e,r,b) is Relation-like NAT -defined A -valued Function-like V51() FinSequence-like FinSubsequence-like FinSequence of A
b + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
mid (e,(b + 1),b) is Relation-like NAT -defined A -valued Function-like V51() FinSequence-like FinSubsequence-like FinSequence of A
(mid (e,r,b)) ^ (mid (e,(b + 1),b)) is Relation-like NAT -defined A -valued Function-like V51() FinSequence-like FinSubsequence-like FinSequence of A
mid (e,r,b) is Relation-like NAT -defined A -valued Function-like V51() FinSequence-like FinSubsequence-like FinSequence of A
len (mid (e,r,b)) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b -' r is V22() real ext-real non negative set
(b -' r) + 1 is non empty V22() real ext-real positive non negative Element of REAL
b - r is V22() real ext-real Element of REAL
(b - r) + 1 is V22() real ext-real Element of REAL
len (mid (e,(b + 1),b)) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b -' (b + 1) is V22() real ext-real non negative set
(b -' (b + 1)) + 1 is non empty V22() real ext-real positive non negative Element of REAL
b - (b + 1) is V22() real ext-real Element of REAL
(b - (b + 1)) + 1 is V22() real ext-real Element of REAL
b - b is V22() real ext-real Element of REAL
len ((mid (e,r,b)) ^ (mid (e,(b + 1),b))) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
((b - r) + 1) + (b - b) is V22() real ext-real Element of REAL
b - r is V22() real ext-real Element of REAL
(b - r) + 1 is V22() real ext-real Element of REAL
c6 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal set
((mid (e,r,b)) ^ (mid (e,(b + 1),b))) . c6 is set
(mid (e,r,b)) . c6 is set
Seg (len ((mid (e,r,b)) ^ (mid (e,(b + 1),b)))) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() len ((mid (e,r,b)) ^ (mid (e,(b + 1),b))) -element bounded_below bounded_above real-bounded Element of K19(NAT)
dom ((mid (e,r,b)) ^ (mid (e,(b + 1),b))) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)
dom (mid (e,r,b)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)
Seg (len (mid (e,r,b))) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() len (mid (e,r,b)) -element bounded_below bounded_above real-bounded Element of K19(NAT)
(mid (e,r,b)) . c6 is set
c6 - 1 is V22() real ext-real Element of REAL
(c6 - 1) + r is V22() real ext-real Element of REAL
e . ((c6 - 1) + r) is set
dom (mid (e,(b + 1),b)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)
X is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal set
(len (mid (e,r,b))) + X is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal set
(len (mid (e,r,b))) + X is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
r - 1 is V22() real ext-real Element of REAL
b - (r - 1) is V22() real ext-real Element of REAL
(b - (r - 1)) + X is V22() real ext-real Element of REAL
((b - (r - 1)) + X) + r is V22() real ext-real Element of REAL
(((b - (r - 1)) + X) + r) - 1 is V22() real ext-real Element of REAL
e . ((((b - (r - 1)) + X) + r) - 1) is set
X + b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
e . (X + b) is set
Seg (len (mid (e,(b + 1),b))) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() len (mid (e,(b + 1),b)) -element bounded_below bounded_above real-bounded Element of K19(NAT)
(mid (e,(b + 1),b)) . X is set
X + (b + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
(X + (b + 1)) - 1 is V22() real ext-real Element of REAL
e . ((X + (b + 1)) - 1) is set
(X + b) + 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
e . ((X + b) + 0) is set
dom (mid (e,r,b)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)
dom (mid (e,(b + 1),b)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)
len (mid (e,r,b)) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b -' r is V22() real ext-real non negative set
(b -' r) + 1 is non empty V22() real ext-real positive non negative Element of REAL
A is complex-membered ext-real-membered real-membered set
e is V22() real ext-real set
e ** A is complex-membered ext-real-membered real-membered set
{e} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{e} ** A is complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {e} & b2 in A ) } is set
{e} ** A is ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {e} & b2 in A ) } is set
e ** A is ext-real-membered set
A is non empty set
K20(A,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(A,REAL)) is V12() V51() set
e is non empty set
r is Relation-like A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
r | A is Relation-like A -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
r | e is Relation-like A -defined e -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
(r | e) | e is Relation-like A -defined e -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
dom r is Element of K19(A)
K19(A) is set
A /\ (dom r) is Element of K19(A)
b is V22() real ext-real set
dom (r | e) is Element of K19(A)
e /\ (dom (r | e)) is Element of K19(A)
b is set
(r | e) . b is V22() real ext-real Element of REAL
(dom r) /\ e is Element of K19(A)
(dom r) /\ A is Element of K19(A)
r . b is V22() real ext-real Element of REAL
A is non empty set
K20(A,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(A,REAL)) is V12() V51() set
e is non empty set
r is Relation-like A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
r | A is Relation-like A -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
r | e is Relation-like A -defined e -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
(r | e) | e is Relation-like A -defined e -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
dom r is Element of K19(A)
K19(A) is set
A /\ (dom r) is Element of K19(A)
b is V22() real ext-real set
dom (r | e) is Element of K19(A)
e /\ (dom (r | e)) is Element of K19(A)
b is set
(r | e) . b is V22() real ext-real Element of REAL
(dom r) /\ e is Element of K19(A)
(dom r) /\ A is Element of K19(A)
r . b is V22() real ext-real Element of REAL
A is complex-membered ext-real-membered real-membered set
e is V22() real ext-real set
(A,e) is complex-membered ext-real-membered real-membered Element of K19(REAL)
{e} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{e} ** A is complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {e} & b2 in A ) } is set
{e} ** A is ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {e} & b2 in A ) } is set
e ** A is ext-real-membered set
r is complex-membered ext-real-membered real-membered set
b is V22() real ext-real set
(r,b) is complex-membered ext-real-membered real-membered Element of K19(REAL)
{b} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{b} ** r is complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {b} & b2 in r ) } is set
{b} ** r is ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {b} & b2 in r ) } is set
b ** r is ext-real-membered set
A is V22() real ext-real Element of REAL
e is complex-membered ext-real-membered real-membered Element of K19(REAL)
(e,A) is complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** e is complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in e ) } is set
{A} ** e is ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in e ) } is set
A ** e is ext-real-membered set
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in e } is set
r is set
b is ext-real Element of ExtREAL
A * b is ext-real set
b is V22() real ext-real Element of REAL
A * b is V22() real ext-real Element of REAL
r is set
b is V22() real ext-real Element of REAL
A * b is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** e is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in e ) } is set
{A} ** e is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in e ) } is set
A ** e is non empty ext-real-membered set
r is V22() real ext-real set
b is V22() real ext-real set
A * r is V22() real ext-real Element of REAL
b is ext-real set
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in e } is set
b is V22() real ext-real Element of REAL
A * b is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** e is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in e ) } is set
{A} ** e is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in e ) } is set
A ** e is non empty ext-real-membered set
r is V22() real ext-real set
b is V22() real ext-real set
A * r is V22() real ext-real Element of REAL
b is ext-real set
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in e } is set
b is V22() real ext-real Element of REAL
A * b is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** e is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in e ) } is set
{A} ** e is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in e ) } is set
A ** e is non empty ext-real-membered set
r is V22() real ext-real set
b is V22() real ext-real set
A * r is V22() real ext-real Element of REAL
b is ext-real set
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in e } is set
b is V22() real ext-real Element of REAL
A * b is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** e is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in e ) } is set
{A} ** e is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in e ) } is set
A ** e is non empty ext-real-membered set
r is V22() real ext-real set
b is V22() real ext-real set
A * r is V22() real ext-real Element of REAL
b is ext-real set
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in e } is set
b is V22() real ext-real Element of REAL
A * b is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** e is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in e ) } is set
{A} ** e is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in e ) } is set
A ** e is non empty ext-real-membered set
upper_bound (e,A) is V22() real ext-real Element of REAL
upper_bound e is V22() real ext-real Element of REAL
A * (upper_bound e) is V22() real ext-real Element of REAL
r is V22() real ext-real set
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in e } is set
b is V22() real ext-real Element of REAL
A * b is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
b is V22() real ext-real set
A * r is V22() real ext-real Element of REAL
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in e } is set
b / A is V22() real ext-real Element of REAL
b is V22() real ext-real set
A * b is V22() real ext-real Element of REAL
(b / A) * A is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** e is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in e ) } is set
{A} ** e is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in e ) } is set
A ** e is non empty ext-real-membered set
lower_bound (e,A) is V22() real ext-real Element of REAL
upper_bound e is V22() real ext-real Element of REAL
A * (upper_bound e) is V22() real ext-real Element of REAL
r is V22() real ext-real set
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in e } is set
b is V22() real ext-real Element of REAL
A * b is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
b is V22() real ext-real set
A * r is V22() real ext-real Element of REAL
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in e } is set
b / A is V22() real ext-real Element of REAL
b is V22() real ext-real set
A * b is V22() real ext-real Element of REAL
(b / A) * A is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** e is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in e ) } is set
{A} ** e is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in e ) } is set
A ** e is non empty ext-real-membered set
lower_bound (e,A) is V22() real ext-real Element of REAL
lower_bound e is V22() real ext-real Element of REAL
A * (lower_bound e) is V22() real ext-real Element of REAL
r is V22() real ext-real set
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in e } is set
b is V22() real ext-real Element of REAL
A * b is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
b is V22() real ext-real set
A * r is V22() real ext-real Element of REAL
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in e } is set
b / A is V22() real ext-real Element of REAL
b is V22() real ext-real set
A * b is V22() real ext-real Element of REAL
(b / A) * A is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** e is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in e ) } is set
{A} ** e is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in e ) } is set
A ** e is non empty ext-real-membered set
upper_bound (e,A) is V22() real ext-real Element of REAL
lower_bound e is V22() real ext-real Element of REAL
A * (lower_bound e) is V22() real ext-real Element of REAL
r is V22() real ext-real set
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in e } is set
b is V22() real ext-real Element of REAL
A * b is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
b is V22() real ext-real set
A * r is V22() real ext-real Element of REAL
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in e } is set
b / A is V22() real ext-real Element of REAL
b is V22() real ext-real set
A * b is V22() real ext-real Element of REAL
(b / A) * A is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty set
K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(e,REAL)) is V12() V51() set
r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
A (#) r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
rng (A (#) r) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
rng r is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
((rng r),A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** (rng r) is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in rng r ) } is set
{A} ** (rng r) is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in rng r ) } is set
A ** (rng r) is non empty ext-real-membered set
b is V22() real ext-real Element of REAL
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in rng r } is set
b is V22() real ext-real Element of REAL
A * b is V22() real ext-real Element of REAL
dom r is non empty Element of K19(e)
K19(e) is set
c6 is Element of e
r . c6 is V22() real ext-real Element of REAL
dom (A (#) r) is non empty Element of K19(e)
(A (#) r) . c6 is V22() real ext-real Element of REAL
b is V22() real ext-real Element of REAL
dom (A (#) r) is non empty Element of K19(e)
K19(e) is set
b is Element of e
(A (#) r) . b is V22() real ext-real Element of REAL
dom r is non empty Element of K19(e)
r . b is V22() real ext-real Element of REAL
A * (r . b) is V22() real ext-real Element of REAL
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in rng r } is set
A is V22() real ext-real Element of REAL
e is non empty set
K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(e,REAL)) is V12() V51() set
r is non empty set
b is Relation-like e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
b | r is Relation-like e -defined r -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
A (#) (b | r) is Relation-like e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
rng (A (#) (b | r)) is complex-membered ext-real-membered real-membered Element of K19(REAL)
rng (b | r) is complex-membered ext-real-membered real-membered Element of K19(REAL)
((rng (b | r)),A) is complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** (rng (b | r)) is complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in rng (b | r) ) } is set
{A} ** (rng (b | r)) is ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in rng (b | r) ) } is set
A ** (rng (b | r)) is ext-real-membered set
b is V22() real ext-real Element of REAL
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in rng (b | r) } is set
c6 is V22() real ext-real Element of REAL
A * c6 is V22() real ext-real Element of REAL
dom (b | r) is Element of K19(e)
K19(e) is set
X is Element of e
(b | r) . X is V22() real ext-real Element of REAL
dom (A (#) (b | r)) is Element of K19(e)
(A (#) (b | r)) . X is V22() real ext-real Element of REAL
b is V22() real ext-real Element of REAL
dom (A (#) (b | r)) is Element of K19(e)
K19(e) is set
c6 is Element of e
(A (#) (b | r)) . c6 is V22() real ext-real Element of REAL
dom (b | r) is Element of K19(e)
(b | r) . c6 is V22() real ext-real Element of REAL
A * ((b | r) . c6) is V22() real ext-real Element of REAL
{ (A * b1) where b1 is V22() real ext-real Element of REAL : b1 in rng (b | r) } is set
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(e,REAL)) is V12() V51() set
vol e is V22() real ext-real Element of REAL
r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
r | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
rng r is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
lower_bound (rng r) is V22() real ext-real Element of REAL
A * (lower_bound (rng r)) is V22() real ext-real Element of REAL
(A * (lower_bound (rng r))) * (vol e) is V22() real ext-real Element of REAL
A (#) r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
upper_sum_set (A (#) r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
divs e is non empty set
K20((divs e),REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20((divs e),REAL)) is V12() V51() set
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e
(upper_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
(A (#) r) | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
rng (A (#) r) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
lower_bound (rng (A (#) r)) is V22() real ext-real Element of REAL
(lower_bound (rng (A (#) r))) * (vol e) is V22() real ext-real Element of REAL
lower_sum ((A (#) r),b) is V22() real ext-real Element of REAL
upper_sum ((A (#) r),b) is V22() real ext-real Element of REAL
((rng r),A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** (rng r) is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in rng r ) } is set
{A} ** (rng r) is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in rng r ) } is set
A ** (rng r) is non empty ext-real-membered set
lower_bound ((rng r),A) is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(e,REAL)) is V12() V51() set
vol e is V22() real ext-real Element of REAL
r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
r | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
rng r is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
upper_bound (rng r) is V22() real ext-real Element of REAL
A * (upper_bound (rng r)) is V22() real ext-real Element of REAL
(A * (upper_bound (rng r))) * (vol e) is V22() real ext-real Element of REAL
A (#) r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
upper_sum_set (A (#) r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
divs e is non empty set
K20((divs e),REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20((divs e),REAL)) is V12() V51() set
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e
(upper_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
(A (#) r) | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
rng (A (#) r) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
lower_bound (rng (A (#) r)) is V22() real ext-real Element of REAL
(lower_bound (rng (A (#) r))) * (vol e) is V22() real ext-real Element of REAL
lower_sum ((A (#) r),b) is V22() real ext-real Element of REAL
upper_sum ((A (#) r),b) is V22() real ext-real Element of REAL
((rng r),A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** (rng r) is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in rng r ) } is set
{A} ** (rng r) is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in rng r ) } is set
A ** (rng r) is non empty ext-real-membered set
lower_bound ((rng r),A) is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(e,REAL)) is V12() V51() set
vol e is V22() real ext-real Element of REAL
r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
r | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
A (#) r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
lower_sum_set (A (#) r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
divs e is non empty set
K20((divs e),REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20((divs e),REAL)) is V12() V51() set
rng r is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
upper_bound (rng r) is V22() real ext-real Element of REAL
A * (upper_bound (rng r)) is V22() real ext-real Element of REAL
(A * (upper_bound (rng r))) * (vol e) is V22() real ext-real Element of REAL
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e
(lower_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
(A (#) r) | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
upper_sum ((A (#) r),b) is V22() real ext-real Element of REAL
rng (A (#) r) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
upper_bound (rng (A (#) r)) is V22() real ext-real Element of REAL
(upper_bound (rng (A (#) r))) * (vol e) is V22() real ext-real Element of REAL
lower_sum ((A (#) r),b) is V22() real ext-real Element of REAL
((rng r),A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** (rng r) is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in rng r ) } is set
{A} ** (rng r) is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in rng r ) } is set
A ** (rng r) is non empty ext-real-membered set
upper_bound ((rng r),A) is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(e,REAL)) is V12() V51() set
vol e is V22() real ext-real Element of REAL
r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
r | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
A (#) r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
lower_sum_set (A (#) r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
divs e is non empty set
K20((divs e),REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20((divs e),REAL)) is V12() V51() set
rng r is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
lower_bound (rng r) is V22() real ext-real Element of REAL
A * (lower_bound (rng r)) is V22() real ext-real Element of REAL
(A * (lower_bound (rng r))) * (vol e) is V22() real ext-real Element of REAL
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e
(lower_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
(A (#) r) | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
upper_sum ((A (#) r),b) is V22() real ext-real Element of REAL
rng (A (#) r) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
upper_bound (rng (A (#) r)) is V22() real ext-real Element of REAL
(upper_bound (rng (A (#) r))) * (vol e) is V22() real ext-real Element of REAL
lower_sum ((A (#) r),b) is V22() real ext-real Element of REAL
((rng r),A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** (rng r) is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in rng r ) } is set
{A} ** (rng r) is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in rng r ) } is set
A ** (rng r) is non empty ext-real-membered set
upper_bound ((rng r),A) is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
r is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(r,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(r,REAL)) is V12() V51() set
b is Relation-like r -defined REAL -valued Function-like non empty total V30(r, REAL ) V34() V35() V36() Element of K19(K20(r,REAL))
b | r is Relation-like r -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
A (#) b is Relation-like r -defined REAL -valued Function-like non empty total V30(r, REAL ) V34() V35() V36() Element of K19(K20(r,REAL))
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of r
dom b is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
upper_volume ((A (#) b),b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
(upper_volume ((A (#) b),b)) . e is V22() real ext-real Element of REAL
upper_volume (b,b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
(upper_volume (b,b)) . e is V22() real ext-real Element of REAL
A * ((upper_volume (b,b)) . e) is V22() real ext-real Element of REAL
divset (b,e) is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
b | (divset (b,e)) is Relation-like r -defined divset (b,e) -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
dom (b | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(r)
K19(r) is set
dom b is non empty complex-membered ext-real-membered real-membered Element of K19(r)
(dom b) /\ (divset (b,e)) is complex-membered ext-real-membered real-membered Element of K19(REAL)
r /\ (divset (b,e)) is complex-membered ext-real-membered real-membered interval Element of K19(REAL)
rng (b | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(REAL)
rng b is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
(A (#) b) | (divset (b,e)) is Relation-like r -defined divset (b,e) -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
rng ((A (#) b) | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(REAL)
upper_bound (rng ((A (#) b) | (divset (b,e)))) is V22() real ext-real Element of REAL
vol (divset (b,e)) is V22() real ext-real Element of REAL
(upper_bound (rng ((A (#) b) | (divset (b,e))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
A (#) (b | (divset (b,e))) is Relation-like r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
rng (A (#) (b | (divset (b,e)))) is complex-membered ext-real-membered real-membered Element of K19(REAL)
upper_bound (rng (A (#) (b | (divset (b,e))))) is V22() real ext-real Element of REAL
(upper_bound (rng (A (#) (b | (divset (b,e)))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
((rng (b | (divset (b,e)))),A) is complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** (rng (b | (divset (b,e)))) is complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in rng (b | (divset (b,e))) ) } is set
{A} ** (rng (b | (divset (b,e)))) is ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in rng (b | (divset (b,e))) ) } is set
A ** (rng (b | (divset (b,e)))) is ext-real-membered set
upper_bound ((rng (b | (divset (b,e)))),A) is V22() real ext-real Element of REAL
(upper_bound ((rng (b | (divset (b,e)))),A)) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
upper_bound (rng (b | (divset (b,e)))) is V22() real ext-real Element of REAL
A * (upper_bound (rng (b | (divset (b,e))))) is V22() real ext-real Element of REAL
(A * (upper_bound (rng (b | (divset (b,e)))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
(upper_bound (rng (b | (divset (b,e))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
A * ((upper_bound (rng (b | (divset (b,e))))) * (vol (divset (b,e)))) is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
r is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(r,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(r,REAL)) is V12() V51() set
b is Relation-like r -defined REAL -valued Function-like non empty total V30(r, REAL ) V34() V35() V36() Element of K19(K20(r,REAL))
b | r is Relation-like r -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
A (#) b is Relation-like r -defined REAL -valued Function-like non empty total V30(r, REAL ) V34() V35() V36() Element of K19(K20(r,REAL))
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of r
dom b is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
lower_volume ((A (#) b),b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
(lower_volume ((A (#) b),b)) . e is V22() real ext-real Element of REAL
upper_volume (b,b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
(upper_volume (b,b)) . e is V22() real ext-real Element of REAL
A * ((upper_volume (b,b)) . e) is V22() real ext-real Element of REAL
divset (b,e) is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
b | (divset (b,e)) is Relation-like r -defined divset (b,e) -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
dom (b | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(r)
K19(r) is set
dom b is non empty complex-membered ext-real-membered real-membered Element of K19(r)
(dom b) /\ (divset (b,e)) is complex-membered ext-real-membered real-membered Element of K19(REAL)
r /\ (divset (b,e)) is complex-membered ext-real-membered real-membered interval Element of K19(REAL)
rng (b | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(REAL)
rng b is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
(A (#) b) | (divset (b,e)) is Relation-like r -defined divset (b,e) -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
rng ((A (#) b) | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(REAL)
lower_bound (rng ((A (#) b) | (divset (b,e)))) is V22() real ext-real Element of REAL
vol (divset (b,e)) is V22() real ext-real Element of REAL
(lower_bound (rng ((A (#) b) | (divset (b,e))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
A (#) (b | (divset (b,e))) is Relation-like r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
rng (A (#) (b | (divset (b,e)))) is complex-membered ext-real-membered real-membered Element of K19(REAL)
lower_bound (rng (A (#) (b | (divset (b,e))))) is V22() real ext-real Element of REAL
(lower_bound (rng (A (#) (b | (divset (b,e)))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
((rng (b | (divset (b,e)))),A) is complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** (rng (b | (divset (b,e)))) is complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in rng (b | (divset (b,e))) ) } is set
{A} ** (rng (b | (divset (b,e)))) is ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in rng (b | (divset (b,e))) ) } is set
A ** (rng (b | (divset (b,e)))) is ext-real-membered set
lower_bound ((rng (b | (divset (b,e)))),A) is V22() real ext-real Element of REAL
(lower_bound ((rng (b | (divset (b,e)))),A)) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
upper_bound (rng (b | (divset (b,e)))) is V22() real ext-real Element of REAL
A * (upper_bound (rng (b | (divset (b,e))))) is V22() real ext-real Element of REAL
(A * (upper_bound (rng (b | (divset (b,e)))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
(upper_bound (rng (b | (divset (b,e))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
A * ((upper_bound (rng (b | (divset (b,e))))) * (vol (divset (b,e)))) is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
r is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(r,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(r,REAL)) is V12() V51() set
b is Relation-like r -defined REAL -valued Function-like non empty total V30(r, REAL ) V34() V35() V36() Element of K19(K20(r,REAL))
b | r is Relation-like r -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
A (#) b is Relation-like r -defined REAL -valued Function-like non empty total V30(r, REAL ) V34() V35() V36() Element of K19(K20(r,REAL))
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of r
dom b is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
lower_volume ((A (#) b),b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
(lower_volume ((A (#) b),b)) . e is V22() real ext-real Element of REAL
lower_volume (b,b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
(lower_volume (b,b)) . e is V22() real ext-real Element of REAL
A * ((lower_volume (b,b)) . e) is V22() real ext-real Element of REAL
divset (b,e) is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
b | (divset (b,e)) is Relation-like r -defined divset (b,e) -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
dom (b | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(r)
K19(r) is set
dom b is non empty complex-membered ext-real-membered real-membered Element of K19(r)
(dom b) /\ (divset (b,e)) is complex-membered ext-real-membered real-membered Element of K19(REAL)
r /\ (divset (b,e)) is complex-membered ext-real-membered real-membered interval Element of K19(REAL)
rng (b | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(REAL)
rng b is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
(A (#) b) | (divset (b,e)) is Relation-like r -defined divset (b,e) -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
rng ((A (#) b) | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(REAL)
lower_bound (rng ((A (#) b) | (divset (b,e)))) is V22() real ext-real Element of REAL
vol (divset (b,e)) is V22() real ext-real Element of REAL
(lower_bound (rng ((A (#) b) | (divset (b,e))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
A (#) (b | (divset (b,e))) is Relation-like r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
rng (A (#) (b | (divset (b,e)))) is complex-membered ext-real-membered real-membered Element of K19(REAL)
lower_bound (rng (A (#) (b | (divset (b,e))))) is V22() real ext-real Element of REAL
(lower_bound (rng (A (#) (b | (divset (b,e)))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
((rng (b | (divset (b,e)))),A) is complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** (rng (b | (divset (b,e)))) is complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in rng (b | (divset (b,e))) ) } is set
{A} ** (rng (b | (divset (b,e)))) is ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in rng (b | (divset (b,e))) ) } is set
A ** (rng (b | (divset (b,e)))) is ext-real-membered set
lower_bound ((rng (b | (divset (b,e)))),A) is V22() real ext-real Element of REAL
(lower_bound ((rng (b | (divset (b,e)))),A)) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
lower_bound (rng (b | (divset (b,e)))) is V22() real ext-real Element of REAL
A * (lower_bound (rng (b | (divset (b,e))))) is V22() real ext-real Element of REAL
(A * (lower_bound (rng (b | (divset (b,e)))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
(lower_bound (rng (b | (divset (b,e))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
A * ((lower_bound (rng (b | (divset (b,e))))) * (vol (divset (b,e)))) is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
r is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(r,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(r,REAL)) is V12() V51() set
b is Relation-like r -defined REAL -valued Function-like non empty total V30(r, REAL ) V34() V35() V36() Element of K19(K20(r,REAL))
b | r is Relation-like r -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
A (#) b is Relation-like r -defined REAL -valued Function-like non empty total V30(r, REAL ) V34() V35() V36() Element of K19(K20(r,REAL))
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of r
dom b is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
upper_volume ((A (#) b),b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
(upper_volume ((A (#) b),b)) . e is V22() real ext-real Element of REAL
lower_volume (b,b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
(lower_volume (b,b)) . e is V22() real ext-real Element of REAL
A * ((lower_volume (b,b)) . e) is V22() real ext-real Element of REAL
divset (b,e) is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
b | (divset (b,e)) is Relation-like r -defined divset (b,e) -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
dom (b | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(r)
K19(r) is set
dom b is non empty complex-membered ext-real-membered real-membered Element of K19(r)
(dom b) /\ (divset (b,e)) is complex-membered ext-real-membered real-membered Element of K19(REAL)
r /\ (divset (b,e)) is complex-membered ext-real-membered real-membered interval Element of K19(REAL)
rng (b | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(REAL)
rng b is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
(A (#) b) | (divset (b,e)) is Relation-like r -defined divset (b,e) -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
rng ((A (#) b) | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(REAL)
upper_bound (rng ((A (#) b) | (divset (b,e)))) is V22() real ext-real Element of REAL
vol (divset (b,e)) is V22() real ext-real Element of REAL
(upper_bound (rng ((A (#) b) | (divset (b,e))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
A (#) (b | (divset (b,e))) is Relation-like r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))
rng (A (#) (b | (divset (b,e)))) is complex-membered ext-real-membered real-membered Element of K19(REAL)
upper_bound (rng (A (#) (b | (divset (b,e))))) is V22() real ext-real Element of REAL
(upper_bound (rng (A (#) (b | (divset (b,e)))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
((rng (b | (divset (b,e)))),A) is complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** (rng (b | (divset (b,e)))) is complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in rng (b | (divset (b,e))) ) } is set
{A} ** (rng (b | (divset (b,e)))) is ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in rng (b | (divset (b,e))) ) } is set
A ** (rng (b | (divset (b,e)))) is ext-real-membered set
upper_bound ((rng (b | (divset (b,e)))),A) is V22() real ext-real Element of REAL
(upper_bound ((rng (b | (divset (b,e)))),A)) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
lower_bound (rng (b | (divset (b,e)))) is V22() real ext-real Element of REAL
A * (lower_bound (rng (b | (divset (b,e))))) is V22() real ext-real Element of REAL
(A * (lower_bound (rng (b | (divset (b,e)))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
(lower_bound (rng (b | (divset (b,e))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL
A * ((lower_bound (rng (b | (divset (b,e))))) * (vol (divset (b,e)))) is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(e,REAL)) is V12() V51() set
r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
r | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
A (#) r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e
upper_sum ((A (#) r),b) is V22() real ext-real Element of REAL
upper_sum (r,b) is V22() real ext-real Element of REAL
A * (upper_sum (r,b)) is V22() real ext-real Element of REAL
upper_volume ((A (#) r),b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
len (upper_volume ((A (#) r),b)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
upper_volume (r,b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
A * (upper_volume (r,b)) is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal set
(upper_volume ((A (#) r),b)) . b is V22() real ext-real Element of REAL
(A * (upper_volume (r,b))) . b is V22() real ext-real Element of REAL
len b is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom b is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
(upper_volume (r,b)) . b is V22() real ext-real Element of REAL
A * ((upper_volume (r,b)) . b) is V22() real ext-real Element of REAL
len b is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len (upper_volume (r,b)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len (A * (upper_volume (r,b))) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
Sum (A * (upper_volume (r,b))) is V22() real ext-real Element of REAL
Sum (upper_volume (r,b)) is V22() real ext-real Element of REAL
A * (Sum (upper_volume (r,b))) is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(e,REAL)) is V12() V51() set
r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
r | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
A (#) r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e
lower_sum ((A (#) r),b) is V22() real ext-real Element of REAL
upper_sum (r,b) is V22() real ext-real Element of REAL
A * (upper_sum (r,b)) is V22() real ext-real Element of REAL
lower_volume ((A (#) r),b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
len (lower_volume ((A (#) r),b)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
upper_volume (r,b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
A * (upper_volume (r,b)) is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal set
(lower_volume ((A (#) r),b)) . b is V22() real ext-real Element of REAL
(A * (upper_volume (r,b))) . b is V22() real ext-real Element of REAL
len b is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom b is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
(upper_volume (r,b)) . b is V22() real ext-real Element of REAL
A * ((upper_volume (r,b)) . b) is V22() real ext-real Element of REAL
len b is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len (upper_volume (r,b)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len (A * (upper_volume (r,b))) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
Sum (A * (upper_volume (r,b))) is V22() real ext-real Element of REAL
Sum (upper_volume (r,b)) is V22() real ext-real Element of REAL
A * (Sum (upper_volume (r,b))) is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(e,REAL)) is V12() V51() set
r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
r | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
A (#) r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e
lower_sum ((A (#) r),b) is V22() real ext-real Element of REAL
lower_sum (r,b) is V22() real ext-real Element of REAL
A * (lower_sum (r,b)) is V22() real ext-real Element of REAL
lower_volume ((A (#) r),b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
len (lower_volume ((A (#) r),b)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
lower_volume (r,b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
A * (lower_volume (r,b)) is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal set
(lower_volume ((A (#) r),b)) . b is V22() real ext-real Element of REAL
(A * (lower_volume (r,b))) . b is V22() real ext-real Element of REAL
len b is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom b is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
(lower_volume (r,b)) . b is V22() real ext-real Element of REAL
A * ((lower_volume (r,b)) . b) is V22() real ext-real Element of REAL
len b is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len (lower_volume (r,b)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len (A * (lower_volume (r,b))) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
Sum (A * (lower_volume (r,b))) is V22() real ext-real Element of REAL
Sum (lower_volume (r,b)) is V22() real ext-real Element of REAL
A * (Sum (lower_volume (r,b))) is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(e,REAL)) is V12() V51() set
r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
r | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
A (#) r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e
upper_sum ((A (#) r),b) is V22() real ext-real Element of REAL
lower_sum (r,b) is V22() real ext-real Element of REAL
A * (lower_sum (r,b)) is V22() real ext-real Element of REAL
upper_volume ((A (#) r),b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
len (upper_volume ((A (#) r),b)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
lower_volume (r,b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
A * (lower_volume (r,b)) is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal set
(upper_volume ((A (#) r),b)) . b is V22() real ext-real Element of REAL
(A * (lower_volume (r,b))) . b is V22() real ext-real Element of REAL
len b is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom b is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
(lower_volume (r,b)) . b is V22() real ext-real Element of REAL
A * ((lower_volume (r,b)) . b) is V22() real ext-real Element of REAL
len b is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len (lower_volume (r,b)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len (A * (lower_volume (r,b))) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
Sum (A * (lower_volume (r,b))) is V22() real ext-real Element of REAL
Sum (lower_volume (r,b)) is V22() real ext-real Element of REAL
A * (Sum (lower_volume (r,b))) is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(e,REAL)) is V12() V51() set
r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
r | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))
A (#) r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))
integral (A (#) r) is V22() real ext-real Element of REAL
integral r is V22() real ext-real Element of REAL
A * (integral r) is V22() real ext-real Element of REAL
upper_sum_set r is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
divs e is non empty set
K20((divs e),REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20((divs e),REAL)) is V12() V51() set
rng (upper_sum_set r) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
lower_sum_set r is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
rng (lower_sum_set r) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
upper_sum_set (A (#) r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
A (#) (upper_sum_set r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
b is set
(upper_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
(A (#) (upper_sum_set r)) . b is V22() real ext-real Element of REAL
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e
(upper_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
upper_sum ((A (#) r),b) is V22() real ext-real Element of REAL
upper_sum (r,b) is V22() real ext-real Element of REAL
A * (upper_sum (r,b)) is V22() real ext-real Element of REAL
(upper_sum_set r) . b is V22() real ext-real Element of REAL
A * ((upper_sum_set r) . b) is V22() real ext-real Element of REAL
(A (#) (upper_sum_set r)) . b is V22() real ext-real Element of REAL
dom (upper_sum_set r) is non empty Element of K19((divs e))
K19((divs e)) is set
dom (A (#) (upper_sum_set r)) is non empty Element of K19((divs e))
dom (upper_sum_set (A (#) r)) is non empty Element of K19((divs e))
upper_integral (A (#) r) is V22() real ext-real Element of REAL
rng (A (#) (upper_sum_set r)) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
lower_bound (rng (A (#) (upper_sum_set r))) is V22() real ext-real Element of REAL
((rng (upper_sum_set r)),A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** (rng (upper_sum_set r)) is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in rng (upper_sum_set r) ) } is set
{A} ** (rng (upper_sum_set r)) is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in rng (upper_sum_set r) ) } is set
A ** (rng (upper_sum_set r)) is non empty ext-real-membered set
lower_bound ((rng (upper_sum_set r)),A) is V22() real ext-real Element of REAL
lower_bound (rng (upper_sum_set r)) is V22() real ext-real Element of REAL
A * (lower_bound (rng (upper_sum_set r))) is V22() real ext-real Element of REAL
upper_integral r is V22() real ext-real Element of REAL
A * (upper_integral r) is V22() real ext-real Element of REAL
lower_sum_set (A (#) r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
A (#) (lower_sum_set r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
b is set
(lower_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
(A (#) (lower_sum_set r)) . b is V22() real ext-real Element of REAL
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e
(lower_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
lower_sum ((A (#) r),b) is V22() real ext-real Element of REAL
lower_sum (r,b) is V22() real ext-real Element of REAL
A * (lower_sum (r,b)) is V22() real ext-real Element of REAL
(lower_sum_set r) . b is V22() real ext-real Element of REAL
A * ((lower_sum_set r) . b) is V22() real ext-real Element of REAL
(A (#) (lower_sum_set r)) . b is V22() real ext-real Element of REAL
dom (lower_sum_set r) is non empty Element of K19((divs e))
dom (A (#) (lower_sum_set r)) is non empty Element of K19((divs e))
dom (lower_sum_set (A (#) r)) is non empty Element of K19((divs e))
lower_integral (A (#) r) is V22() real ext-real Element of REAL
rng (A (#) (lower_sum_set r)) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
upper_bound (rng (A (#) (lower_sum_set r))) is V22() real ext-real Element of REAL
((rng (lower_sum_set r)),A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} ** (rng (lower_sum_set r)) is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in rng (lower_sum_set r) ) } is set
{A} ** (rng (lower_sum_set r)) is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in rng (lower_sum_set r) ) } is set
A ** (rng (lower_sum_set r)) is non empty ext-real-membered set
upper_bound ((rng (lower_sum_set r)),A) is V22() real ext-real Element of REAL
upper_bound (rng (lower_sum_set r)) is V22() real ext-real Element of REAL
A * (upper_bound (rng (lower_sum_set r))) is V22() real ext-real Element of REAL
lower_integral r is V22() real ext-real Element of REAL
A * (lower_integral r) is V22() real ext-real Element of REAL
upper_sum_set (A (#) r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
A (#) (lower_sum_set r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
b is set
(upper_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
(A (#) (lower_sum_set r)) . b is V22() real ext-real Element of REAL
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e
(upper_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
upper_sum ((A (#) r),b) is V22() real ext-real Element of REAL
lower_sum (r,b) is V22() real ext-real Element of REAL
A * (lower_sum (r,b)) is V22() real ext-real Element of REAL
(lower_sum_set r) . b is V22() real ext-real Element of REAL
A * ((lower_sum_set r) . b) is V22() real ext-real Element of REAL
(A (#) (lower_sum_set r)) . b is V22() real ext-real Element of REAL
dom (lower_sum_set r) is non empty Element of K19((divs e))
K19((divs e)) is set
dom (A (#) (lower_sum_set r)) is non empty Element of K19((divs e))
dom (upper_sum_set (A (#) r)) is non empty Element of K19((divs e))
upper_integral (A (#) r) is V22() real ext-real Element of REAL
rng (A (#) (lower_sum_set r)) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
lower_bound (rng (A (#) (lower_sum_set r))) is V22() real ext-real Element of REAL
((rng (lower_sum_set r)),A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{A} ** (rng (lower_sum_set r)) is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in rng (lower_sum_set r) ) } is set
{A} ** (rng (lower_sum_set r)) is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in rng (lower_sum_set r) ) } is set
A ** (rng (lower_sum_set r)) is non empty ext-real-membered set
lower_bound ((rng (lower_sum_set r)),A) is V22() real ext-real Element of REAL
upper_bound (rng (lower_sum_set r)) is V22() real ext-real Element of REAL
A * (upper_bound (rng (lower_sum_set r))) is V22() real ext-real Element of REAL
lower_integral r is V22() real ext-real Element of REAL
A * (lower_integral r) is V22() real ext-real Element of REAL
lower_sum_set (A (#) r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
A (#) (upper_sum_set r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
b is set
(lower_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
(A (#) (upper_sum_set r)) . b is V22() real ext-real Element of REAL
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e
(lower_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
lower_sum ((A (#) r),b) is V22() real ext-real Element of REAL
upper_sum (r,b) is V22() real ext-real Element of REAL
A * (upper_sum (r,b)) is V22() real ext-real Element of REAL
(upper_sum_set r) . b is V22() real ext-real Element of REAL
A * ((upper_sum_set r) . b) is V22() real ext-real Element of REAL
(A (#) (upper_sum_set r)) . b is V22() real ext-real Element of REAL
dom (upper_sum_set r) is non empty Element of K19((divs e))
dom (A (#) (upper_sum_set r)) is non empty Element of K19((divs e))
dom (lower_sum_set (A (#) r)) is non empty Element of K19((divs e))
lower_integral (A (#) r) is V22() real ext-real Element of REAL
rng (A (#) (upper_sum_set r)) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
upper_bound (rng (A (#) (upper_sum_set r))) is V22() real ext-real Element of REAL
((rng (upper_sum_set r)),A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
{A} ** (rng (upper_sum_set r)) is non empty complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {A} & b2 in rng (upper_sum_set r) ) } is set
{A} ** (rng (upper_sum_set r)) is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in rng (upper_sum_set r) ) } is set
A ** (rng (upper_sum_set r)) is non empty ext-real-membered set
upper_bound ((rng (upper_sum_set r)),A) is V22() real ext-real Element of REAL
lower_bound (rng (upper_sum_set r)) is V22() real ext-real Element of REAL
A * (lower_bound (rng (upper_sum_set r))) is V22() real ext-real Element of REAL
upper_integral r is V22() real ext-real Element of REAL
A * (upper_integral r) is V22() real ext-real Element of REAL
upper_integral (A (#) r) is V22() real ext-real Element of REAL
lower_integral (A (#) r) is V22() real ext-real Element of REAL
upper_integral (A (#) r) is V22() real ext-real Element of REAL
lower_integral (A (#) r) is V22() real ext-real Element of REAL
lower_sum_set (A (#) r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
dom (lower_sum_set (A (#) r)) is non empty Element of K19((divs e))
K19((divs e)) is set
(divs e) /\ (dom (lower_sum_set (A (#) r))) is Element of K19((divs e))
rng r is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
upper_bound (rng r) is V22() real ext-real Element of REAL
A * (upper_bound (rng r)) is V22() real ext-real Element of REAL
vol e is V22() real ext-real Element of REAL
(A * (upper_bound (rng r))) * (vol e) is V22() real ext-real Element of REAL
b is set
(lower_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
rng r is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
lower_bound (rng r) is V22() real ext-real Element of REAL
A * (lower_bound (rng r)) is V22() real ext-real Element of REAL
vol e is V22() real ext-real Element of REAL
(A * (lower_bound (rng r))) * (vol e) is V22() real ext-real Element of REAL
b is set
(lower_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
b is V22() real ext-real Element of REAL
(lower_sum_set (A (#) r)) | (divs e) is Relation-like divs e -defined divs e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20((divs e),REAL))
b is V22() real ext-real Element of REAL
rng (lower_sum_set (A (#) r)) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
upper_sum_set (A (#) r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))
dom (upper_sum_set (A (#) r)) is non empty Element of K19((divs e))
(divs e) /\ (dom (upper_sum_set (A (#) r))) is Element of K19((divs e))
rng r is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
lower_bound (rng r) is V22() real ext-real Element of REAL
A * (lower_bound (rng r)) is V22() real ext-real Element of REAL
vol e is V22() real ext-real Element of REAL
(A * (lower_bound (rng r))) * (vol e) is V22() real ext-real Element of REAL
b is set
(upper_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
rng r is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
upper_bound (rng r) is V22() real ext-real Element of REAL
A * (upper_bound (rng r)) is V22() real ext-real Element of REAL
vol e is V22() real ext-real Element of REAL
(A * (upper_bound (rng r))) * (vol e) is V22() real ext-real Element of REAL
b is set
(upper_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL
b is V22() real ext-real Element of REAL
(upper_sum_set (A (#) r)) | (divs e) is Relation-like divs e -defined divs e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20((divs e),REAL))
b is V22() real ext-real Element of REAL
rng (upper_sum_set (A (#) r)) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
A is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(A,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(A,REAL)) is V12() V51() set
e is Relation-like A -defined REAL -valued Function-like non empty total V30(A, REAL ) V34() V35() V36() Element of K19(K20(A,REAL))
e | A is Relation-like A -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
integral e is V22() real ext-real Element of REAL
upper_sum_set e is Relation-like divs A -defined REAL -valued Function-like non empty total V30( divs A, REAL ) V34() V35() V36() Element of K19(K20((divs A),REAL))
divs A is non empty set
K20((divs A),REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20((divs A),REAL)) is V12() V51() set
rng (upper_sum_set e) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
r is V22() real ext-real set
dom (upper_sum_set e) is non empty Element of K19((divs A))
K19((divs A)) is set
b is Relation-like NAT -defined Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like Element of divs A
(upper_sum_set e) . b is V22() real ext-real Element of REAL
b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of A
upper_volume (e,b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL
dom (upper_volume (e,b)) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
c6 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal set
(upper_volume (e,b)) . c6 is V22() real ext-real Element of REAL
len b is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len (upper_volume (e,b)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom b is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
divset (b,c6) is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
e | (divset (b,c6)) is Relation-like A -defined divset (b,c6) -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
rng (e | (divset (b,c6))) is complex-membered ext-real-membered real-membered Element of K19(REAL)
upper_bound (rng (e | (divset (b,c6)))) is V22() real ext-real Element of REAL
rng e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
dom (e | (divset (b,c6))) is complex-membered ext-real-membered real-membered Element of K19(A)
K19(A) is set
dom e is non empty complex-membered ext-real-membered real-membered Element of K19(A)
(dom e) /\ (divset (b,c6)) is complex-membered ext-real-membered real-membered Element of K19(REAL)
i is V22() real ext-real Element of REAL
e . i is V22() real ext-real Element of REAL
(e | (divset (b,c6))) . i is V22() real ext-real Element of REAL
vol (divset (b,c6)) is V22() real ext-real Element of REAL
(upper_bound (rng (e | (divset (b,c6))))) * (vol (divset (b,c6))) is V22() real ext-real Element of REAL
upper_sum (e,b) is V22() real ext-real Element of REAL
Sum (upper_volume (e,b)) is V22() real ext-real Element of REAL
upper_integral e is V22() real ext-real Element of REAL
lower_bound (rng (upper_sum_set e)) is V22() real ext-real Element of REAL
A is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(A,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(A,REAL)) is V12() V51() set
e is Relation-like A -defined REAL -valued Function-like non empty total V30(A, REAL ) V34() V35() V36() Element of K19(K20(A,REAL))
e | A is Relation-like A -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
integral e is V22() real ext-real Element of REAL
r is Relation-like A -defined REAL -valued Function-like non empty total V30(A, REAL ) V34() V35() V36() Element of K19(K20(A,REAL))
r | A is Relation-like A -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
e - r is Relation-like A -defined REAL -valued Function-like non empty total V30(A, REAL ) V34() V35() V36() Element of K19(K20(A,REAL))
- r is Relation-like A -defined Function-like total V34() V35() V36() set
K58(1) is V22() real ext-real non positive set
K58(1) * r is Relation-like A -defined Function-like total V34() V35() V36() set
e + (- r) is Relation-like A -defined Function-like total V34() V35() V36() set
integral (e - r) is V22() real ext-real Element of REAL
integral r is V22() real ext-real Element of REAL
(integral e) - (integral r) is V22() real ext-real Element of REAL
- r is Relation-like A -defined REAL -valued Function-like non empty total V30(A, REAL ) V34() V35() V36() Element of K19(K20(A,REAL))
- 1 is V22() real ext-real non positive Element of REAL
(- 1) (#) r is Relation-like A -defined REAL -valued Function-like non empty total V30(A, REAL ) V34() V35() V36() Element of K19(K20(A,REAL))
(- r) | A is Relation-like A -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
integral (- r) is V22() real ext-real Element of REAL
(- 1) * (integral r) is V22() real ext-real Element of REAL
- (integral r) is V22() real ext-real Element of REAL
(integral e) + (- (integral r)) is V22() real ext-real Element of REAL
A is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(A,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(A,REAL)) is V12() V51() set
e is Relation-like A -defined REAL -valued Function-like non empty total V30(A, REAL ) V34() V35() V36() Element of K19(K20(A,REAL))
e | A is Relation-like A -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
integral e is V22() real ext-real Element of REAL
r is Relation-like A -defined REAL -valued Function-like non empty total V30(A, REAL ) V34() V35() V36() Element of K19(K20(A,REAL))
r | A is Relation-like A -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
integral r is V22() real ext-real Element of REAL
e - r is Relation-like A -defined REAL -valued Function-like non empty total V30(A, REAL ) V34() V35() V36() Element of K19(K20(A,REAL))
- r is Relation-like A -defined Function-like total V34() V35() V36() set
K58(1) is V22() real ext-real non positive set
K58(1) * r is Relation-like A -defined Function-like total V34() V35() V36() set
e + (- r) is Relation-like A -defined Function-like total V34() V35() V36() set
dom (e - r) is non empty complex-membered ext-real-membered real-membered Element of K19(A)
K19(A) is set
b is V22() real ext-real Element of REAL
(e - r) . b is V22() real ext-real Element of REAL
e . b is V22() real ext-real Element of REAL
r . b is V22() real ext-real Element of REAL
(e . b) - (r . b) is V22() real ext-real Element of REAL
integral (e - r) is V22() real ext-real Element of REAL
(integral e) - (integral r) is V22() real ext-real Element of REAL
A /\ A is complex-membered ext-real-membered real-membered interval Element of K19(REAL)
(e - r) | (A /\ A) is Relation-like A -defined A /\ A -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
A is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(A,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(A,REAL)) is V12() V51() set
e is Relation-like A -defined REAL -valued Function-like non empty total V30(A, REAL ) V34() V35() V36() Element of K19(K20(A,REAL))
e | A is Relation-like A -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
upper_sum_set e is Relation-like divs A -defined REAL -valued Function-like non empty total V30( divs A, REAL ) V34() V35() V36() Element of K19(K20((divs A),REAL))
divs A is non empty set
K20((divs A),REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20((divs A),REAL)) is V12() V51() set
rng (upper_sum_set e) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
the Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of A is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of A
lower_sum (e, the Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of A) is V22() real ext-real Element of REAL
b is ext-real set
dom (upper_sum_set e) is non empty Element of K19((divs A))
K19((divs A)) is set
b is Relation-like NAT -defined Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like Element of divs A
(upper_sum_set e) . b is V22() real ext-real Element of REAL
c6 is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of A
upper_sum (e,c6) is V22() real ext-real Element of REAL
A is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(A,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(A,REAL)) is V12() V51() set
e is Relation-like A -defined REAL -valued Function-like non empty total V30(A, REAL ) V34() V35() V36() Element of K19(K20(A,REAL))
e | A is Relation-like A -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
lower_sum_set e is Relation-like divs A -defined REAL -valued Function-like non empty total V30( divs A, REAL ) V34() V35() V36() Element of K19(K20((divs A),REAL))
divs A is non empty set
K20((divs A),REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20((divs A),REAL)) is V12() V51() set
rng (lower_sum_set e) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)
the Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of A is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of A
upper_sum (e, the Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of A) is V22() real ext-real Element of REAL
b is ext-real set
dom (lower_sum_set e) is non empty Element of K19((divs A))
K19((divs A)) is set
b is Relation-like NAT -defined Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like Element of divs A
(lower_sum_set e) . b is V22() real ext-real Element of REAL
c6 is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of A
lower_sum (e,c6) is V22() real ext-real Element of REAL
A is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
divs A is non empty set
K20(NAT,(divs A)) is Relation-like V12() V51() set
K19(K20(NAT,(divs A))) is V12() V51() set
e is Relation-like NAT -defined divs A -valued Function-like non empty total V30( NAT , divs A) Element of K19(K20(NAT,(divs A)))
r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
e . r is set
e . r is Relation-like NAT -defined Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like Element of divs A
A is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(A,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(A,REAL)) is V12() V51() set
divs A is non empty set
K20(NAT,(divs A)) is Relation-like V12() V51() set
K19(K20(NAT,(divs A))) is V12() V51() set
K20(NAT,REAL) is Relation-like V12() V34() V35() V36() V51() set
K19(K20(NAT,REAL)) is V12() V51() set
e is Relation-like A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))
r is Relation-like NAT -defined divs A -valued Function-like non empty total V30( NAT , divs A) Element of K19(K20(NAT,(divs A)))
b is Relation-like NAT -defined REAL -valued Function-like non empty total V30( NAT , REAL ) V34() V35() V36() Element of K19(K20(NAT,REAL))
b is Relation-like NAT -defined REAL -valued Function-like non empty total V30( NAT , REAL ) V34() V35() V36() Element of K19(K20(NAT,REAL))
c6 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b . c6 is V22() real ext-real Element of REAL
b . c6 is V22() real ext-real Element of REAL
(A,r,c6) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of A
upper_sum (e,(A,r,c6)) is V22() real ext-real Element of REAL
b is Relation-like NAT -defined REAL -valued Function-like non empty total V30( NAT , REAL ) V34() V35() V36() Element of K19(K20(NAT,REAL))
b is Relation-like NAT -defined REAL -valued Function-like non empty total V30( NAT , REAL ) V34() V35() V36() Element of K19(K20(NAT,REAL))
c6 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b . c6 is V22() real ext-real Element of REAL
b . c6 is V22() real ext-real Element of REAL
(A,r,c6) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of A
lower_sum (e,(A,r,c6)) is V22() real ext-real Element of REAL
A is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
e is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of A
dom e is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
r is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of A
dom r is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
divset (r,b) is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
rng e is non empty complex-membered ext-real-membered real-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
r . b is V22() real ext-real Element of REAL
K19((dom r)) is V51() V55() set
b is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19((dom r))
len r is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
r . (len r) is V22() real ext-real Element of REAL
Seg (len r) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() len r -element left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
len e is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len e) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() len e -element left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
upper_bound A is V22() real ext-real Element of REAL
e . (len e) is V22() real ext-real Element of REAL
c6 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of K19(NAT)
i is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
r . i is V22() real ext-real Element of REAL
X is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of K19(NAT)
min X is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
r . (min X) is V22() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
e . i is V22() real ext-real Element of REAL
divset (e,i) is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
lower_bound (divset (e,i)) is V22() real ext-real Element of REAL
lower_bound A is V22() real ext-real Element of REAL
upper_bound (divset (e,i)) is V22() real ext-real Element of REAL
[.(lower_bound A),(e . i).] is complex-membered ext-real-membered real-membered interval Element of K19(REAL)
upper_bound A is V22() real ext-real Element of REAL
[.(lower_bound A),(upper_bound A).] is complex-membered ext-real-membered real-membered interval Element of K19(REAL)
{ b1 where b1 is V22() real ext-real Element of REAL : ( lower_bound A <= b1 & b1 <= upper_bound A ) } is set
{ b1 where b1 is V22() real ext-real Element of REAL : ( lower_bound A <= b1 & b1 <= e . i ) } is set
n is V22() real ext-real Element of REAL
rng r is non empty complex-membered ext-real-membered real-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
n is V22() real ext-real Element of REAL
lower_bound (divset (r,b)) is V22() real ext-real Element of REAL
upper_bound (divset (r,b)) is V22() real ext-real Element of REAL
[.(lower_bound A),(r . b).] is complex-membered ext-real-membered real-membered interval Element of K19(REAL)
upper_bound A is V22() real ext-real Element of REAL
[.(lower_bound A),(upper_bound A).] is complex-membered ext-real-membered real-membered interval Element of K19(REAL)
{ b1 where b1 is V22() real ext-real Element of REAL : ( lower_bound A <= b1 & b1 <= upper_bound A ) } is set
rng r is non empty complex-membered ext-real-membered real-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
{ b1 where b1 is V22() real ext-real Element of REAL : ( lower_bound A <= b1 & b1 <= e . i ) } is set
n is V22() real ext-real Element of REAL
b - 1 is V22() real ext-real Element of REAL
r . (b - 1) is V22() real ext-real Element of REAL
b + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
n is V22() real ext-real Element of REAL
lower_bound (divset (r,b)) is V22() real ext-real Element of REAL
upper_bound (divset (r,b)) is V22() real ext-real Element of REAL
[.(r . (b - 1)),(r . b).] is complex-membered ext-real-membered real-membered interval Element of K19(REAL)
len e is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len e) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() len e -element left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
e . 1 is V22() real ext-real Element of REAL
rng r is non empty complex-membered ext-real-membered real-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
r . n is V22() real ext-real Element of REAL
len r is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len r) is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() len r -element left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
b - 1 is V22() real ext-real Element of REAL
i - 1 is V22() real ext-real Element of REAL
e . (i - 1) is V22() real ext-real Element of REAL
r . (b - 1) is V22() real ext-real Element of REAL
rng r is non empty complex-membered ext-real-membered real-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
r . n is V22() real ext-real Element of REAL
n + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
i + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
b + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT
{ b1 where b1 is V22() real ext-real Element of REAL : ( e . (i - 1) <= b1 & b1 <= e . i ) } is set
[.(e . (i - 1)),(e . i).] is complex-membered ext-real-membered real-membered interval Element of K19(REAL)
lower_bound (divset (r,b)) is V22() real ext-real Element of REAL
upper_bound (divset (r,b)) is V22() real ext-real Element of REAL
[.(r . (b - 1)),(r . b).] is complex-membered ext-real-membered real-membered interval Element of K19(REAL)
lower_bound (divset (e,i)) is V22() real ext-real Element of REAL
upper_bound (divset (e,i)) is V22() real ext-real Element of REAL
A is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
vol A is V22() real ext-real Element of REAL
e is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
vol e is V22() real ext-real Element of REAL
upper_bound A is V22() real ext-real Element of REAL
lower_bound A is V22() real ext-real Element of REAL
(upper_bound A) - (lower_bound A) is V22() real ext-real Element of REAL
(vol A) + (lower_bound A) is V22() real ext-real Element of REAL
upper_bound e is V22() real ext-real Element of REAL
(upper_bound e) - (vol A) is V22() real ext-real Element of REAL
lower_bound e is V22() real ext-real Element of REAL
(upper_bound e) - (lower_bound e) is V22() real ext-real Element of REAL
A is complex-membered ext-real-membered real-membered Element of K19(REAL)
r is V22() real ext-real Element of REAL
e is V22() real ext-real Element of REAL
(A,e) is complex-membered ext-real-membered real-membered Element of K19(REAL)
{e} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{e} ** A is complex-membered ext-real-membered real-membered set
{ K193(b1,b2) where b1, b2 is V22() Element of COMPLEX : ( b1 in {e} & b2 in A ) } is set
{e} ** A is ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {e} & b2 in A ) } is set
e ** A is ext-real-membered set
{ (e * b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
b is ext-real Element of ExtREAL
e * b is ext-real set
b is V22() real ext-real Element of REAL
e * b is V22() real ext-real Element of REAL
{0} is non empty V12() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() V55() 1 -element left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
A is non empty ext-real-membered set
0 ** A is non empty ext-real-membered set
{0} is non empty V12() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() V55() 1 -element left_end right_end bounded_below bounded_above real-bounded set
{0} ** A is non empty ext-real-membered set
{ (b1 * b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {0} & b2 in A ) } is set
e is set
r is ext-real set
b is ext-real Element of ExtREAL
0 * b is ext-real set
0 * r is ext-real set