REAL is non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval set
NAT is non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below Element of bool REAL
bool REAL is non empty non trivial V60() set
COMPLEX is non empty non trivial V45() V51() V60() set
RAT is non empty non trivial V45() V46() V47() V48() V51() V60() set
INT is non empty non trivial V45() V46() V47() V48() V49() V51() V60() set
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial V35() V60() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial V60() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial V35() V60() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial V60() set
[:REAL,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:REAL,REAL:] is non empty non trivial V60() set
[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial V60() set
[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial V35() V36() V37() V60() set
bool [:RAT,RAT:] is non empty non trivial V60() set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial V35() V36() V37() V60() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial V60() set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial V35() V36() V37() V60() set
bool [:INT,INT:] is non empty non trivial V60() set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial V35() V36() V37() V60() set
bool [:[:INT,INT:],INT:] is non empty non trivial V60() set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V35() V36() V37() V38() V60() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V35() V36() V37() V38() V60() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial V60() set
{} is Relation-like non-empty empty-yielding RAT -valued V9() empty trivial ordinal natural V22() real ext-real non positive non negative V35() V36() V37() V38() V45() V46() V47() V48() V49() V50() V51() V60() V61() V64() V80() V82( {} ) FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval set
1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
{{},1} is non empty V45() V46() V47() V48() V49() V50() V60() V64() left_end right_end bounded_below bounded_above real-bounded set
ExtREAL is non empty V46() interval set
omega is non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below set
bool omega is non empty non trivial V60() set
bool NAT is non empty non trivial V60() set
[:NAT,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:NAT,REAL:] is non empty non trivial V60() set
[:COMPLEX,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:COMPLEX,REAL:] is non empty non trivial V60() set
2 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
3 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
0 is Relation-like non-empty empty-yielding RAT -valued V9() empty trivial ordinal natural V22() real ext-real non positive non negative V33() V34() V35() V36() V37() V38() V45() V46() V47() V48() V49() V50() V51() V60() V61() V64() V80() V82( {} ) FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval Element of NAT
Seg 1 is non empty trivial V45() V46() V47() V48() V49() V50() V60() V82(1) left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
{1} is non empty trivial V45() V46() V47() V48() V49() V50() V60() V64() V82(1) left_end right_end bounded_below bounded_above real-bounded set
Seg 2 is non empty V45() V46() V47() V48() V49() V50() V60() V82(2) left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
{1,2} is non empty V45() V46() V47() V48() V49() V50() V60() V64() left_end right_end bounded_below bounded_above real-bounded set
addreal is Relation-like [:REAL,REAL:] -defined REAL -valued V6() non empty total V30([:REAL,REAL:], REAL ) V35() V36() V37() Element of bool [:[:REAL,REAL:],REAL:]
diffreal is Relation-like [:REAL,REAL:] -defined REAL -valued V6() non empty total V30([:REAL,REAL:], REAL ) V35() V36() V37() Element of bool [:[:REAL,REAL:],REAL:]
f is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
A is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
g is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
f - g is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
- g is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like set
- 1 is V22() real ext-real non positive set
(- 1) (#) g is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like set
f + (- g) is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like set
Sum (f - g) is V22() real ext-real Element of REAL
X is V22() real ext-real Element of REAL
<*X*> is Relation-like NAT -defined REAL -valued V6() V7() non empty trivial V35() V36() V37() increasing decreasing non-decreasing non-increasing V60() V82(1) FinSequence-like FinSubsequence-like FinSequence of REAL
<*X*> ^ A is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
A ^ <*X*> is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
a1 is V22() real ext-real Element of REAL
<*a1*> is Relation-like NAT -defined REAL -valued V6() V7() non empty trivial V35() V36() V37() increasing decreasing non-decreasing non-increasing V60() V82(1) FinSequence-like FinSubsequence-like FinSequence of REAL
<*a1*> ^ A is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
A ^ <*a1*> is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
X - a1 is V22() real ext-real Element of REAL
len f is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
len A is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
len <*X*> is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len A) + (len <*X*>) is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
(len A) + 1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
len g is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
len <*a1*> is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len <*a1*>) + (len A) is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
1 + (len A) is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
diffreal .: (f,g) is set
len (f - g) is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
dom f is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
b1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
(f - g) . b1 is V22() real ext-real Element of REAL
f /. b1 is V22() real ext-real Element of REAL
g /. b1 is V22() real ext-real Element of REAL
(f /. b1) - (g /. b1) is V22() real ext-real Element of REAL
f . b1 is V22() real ext-real Element of REAL
Seg (len f) is V45() V46() V47() V48() V49() V50() V60() V82( len f) bounded_below bounded_above real-bounded Element of bool NAT
dom g is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
g . b1 is V22() real ext-real Element of REAL
dom (f - g) is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
Sum f is V22() real ext-real Element of REAL
Sum g is V22() real ext-real Element of REAL
(Sum f) - (Sum g) is V22() real ext-real Element of REAL
Sum A is V22() real ext-real Element of REAL
X + (Sum A) is V22() real ext-real Element of REAL
(Sum A) + a1 is V22() real ext-real Element of REAL
A is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len A is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
f is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len f is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
A + f is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len (A + f) is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
A - f is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
- f is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like set
- 1 is V22() real ext-real non positive set
(- 1) (#) f is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like set
A + (- f) is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like set
len (A - f) is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
Sum (A + f) is V22() real ext-real Element of REAL
Sum A is V22() real ext-real Element of REAL
Sum f is V22() real ext-real Element of REAL
(Sum A) + (Sum f) is V22() real ext-real Element of REAL
Sum (A - f) is V22() real ext-real Element of REAL
(Sum A) - (Sum f) is V22() real ext-real Element of REAL
addreal .: (A,f) is set
diffreal .: (A,f) is set
dom A is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
g is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
(A + f) . g is V22() real ext-real Element of REAL
A /. g is V22() real ext-real Element of REAL
f /. g is V22() real ext-real Element of REAL
(A /. g) + (f /. g) is V22() real ext-real Element of REAL
A . g is V22() real ext-real Element of REAL
Seg (len A) is V45() V46() V47() V48() V49() V50() V60() V82( len A) bounded_below bounded_above real-bounded Element of bool NAT
dom f is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
f . g is V22() real ext-real Element of REAL
dom (A + f) is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
g is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
(A - f) . g is V22() real ext-real Element of REAL
A /. g is V22() real ext-real Element of REAL
f /. g is V22() real ext-real Element of REAL
(A /. g) - (f /. g) is V22() real ext-real Element of REAL
A . g is V22() real ext-real Element of REAL
Seg (len A) is V45() V46() V47() V48() V49() V50() V60() V82( len A) bounded_below bounded_above real-bounded Element of bool NAT
dom f is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
f . g is V22() real ext-real Element of REAL
dom (A - f) is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
A is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len A is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
f is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len f is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
dom A is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
Sum A is V22() real ext-real Element of REAL
Sum f is V22() real ext-real Element of REAL
(len A) -tuples_on REAL is V9() non empty FinSequence-membered FinSequenceSet of REAL
Seg (len A) is V45() V46() V47() V48() V49() V50() V60() V82( len A) bounded_below bounded_above real-bounded Element of bool NAT
g is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() V82( len A) FinSequence-like FinSubsequence-like Element of (len A) -tuples_on REAL
X is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() V82( len A) FinSequence-like FinSubsequence-like Element of (len A) -tuples_on REAL
a1 is ordinal natural V22() real ext-real V60() V80() set
g . a1 is V22() real ext-real Element of REAL
X . a1 is V22() real ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f is non empty V45() V46() V47() Element of bool REAL
A | f is Relation-like f -defined REAL -defined REAL -valued V35() V36() V37() set
[:f,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:f,REAL:] is non empty non trivial V60() set
A is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
A (#) f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
g is non empty V45() V46() V47() Element of bool REAL
(A,g) is Relation-like g -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:g,REAL:]
[:g,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:g,REAL:] is non empty non trivial V60() set
(f,g) is Relation-like g -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:g,REAL:]
(A,g) (#) (f,g) is Relation-like REAL -defined g -defined REAL -valued V6() V35() V36() V37() Element of bool [:g,REAL:]
((A (#) f),g) is Relation-like g -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:g,REAL:]
dom ((A (#) f),g) is V45() V46() V47() Element of bool g
bool g is set
dom (A (#) f) is V45() V46() V47() Element of bool REAL
(dom (A (#) f)) /\ g is V45() V46() V47() Element of bool REAL
dom A is V45() V46() V47() Element of bool REAL
dom f is V45() V46() V47() Element of bool REAL
(dom A) /\ (dom f) is V45() V46() V47() Element of bool REAL
((dom A) /\ (dom f)) /\ g is V45() V46() V47() Element of bool REAL
dom ((A,g) (#) (f,g)) is V45() V46() V47() Element of bool g
A | g is Relation-like REAL -defined g -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
dom (A | g) is V45() V46() V47() Element of bool g
dom (f,g) is V45() V46() V47() Element of bool g
(dom (A | g)) /\ (dom (f,g)) is V45() V46() V47() Element of bool g
(dom A) /\ g is V45() V46() V47() Element of bool REAL
f | g is Relation-like REAL -defined g -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
dom (f | g) is V45() V46() V47() Element of bool g
((dom A) /\ g) /\ (dom (f | g)) is V45() V46() V47() Element of bool g
(dom f) /\ g is V45() V46() V47() Element of bool REAL
((dom A) /\ g) /\ ((dom f) /\ g) is V45() V46() V47() Element of bool REAL
((dom A) /\ g) /\ g is V45() V46() V47() Element of bool REAL
(((dom A) /\ g) /\ g) /\ (dom f) is V45() V46() V47() Element of bool REAL
g /\ g is V45() V46() V47() Element of bool REAL
(dom A) /\ (g /\ g) is V45() V46() V47() Element of bool REAL
((dom A) /\ (g /\ g)) /\ (dom f) is V45() V46() V47() Element of bool REAL
((dom A) /\ g) /\ (dom f) is V45() V46() V47() Element of bool REAL
X is V22() real ext-real Element of g
((A,g) (#) (f,g)) . X is V22() real ext-real Element of REAL
((A (#) f),g) . X is V22() real ext-real Element of REAL
(A | g) . X is V22() real ext-real Element of REAL
(f | g) . X is V22() real ext-real Element of REAL
((A | g) . X) * ((f | g) . X) is V22() real ext-real Element of REAL
dom (A,g) is V45() V46() V47() Element of bool g
(dom (A,g)) /\ (dom (f,g)) is V45() V46() V47() Element of bool g
(A (#) f) . X is V22() real ext-real Element of REAL
A . X is V22() real ext-real Element of REAL
f . X is V22() real ext-real Element of REAL
(A . X) * (f . X) is V22() real ext-real Element of REAL
((A | g) . X) * (f . X) is V22() real ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
A + f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
g is non empty V45() V46() V47() Element of bool REAL
((A + f),g) is Relation-like g -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:g,REAL:]
[:g,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:g,REAL:] is non empty non trivial V60() set
(A,g) is Relation-like g -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:g,REAL:]
(f,g) is Relation-like g -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:g,REAL:]
(A,g) + (f,g) is Relation-like REAL -defined g -defined REAL -valued V6() V35() V36() V37() Element of bool [:g,REAL:]
dom ((A,g) + (f,g)) is V45() V46() V47() Element of bool g
bool g is set
A | g is Relation-like REAL -defined g -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
dom (A | g) is V45() V46() V47() Element of bool g
dom (f,g) is V45() V46() V47() Element of bool g
(dom (A | g)) /\ (dom (f,g)) is V45() V46() V47() Element of bool g
dom A is V45() V46() V47() Element of bool REAL
(dom A) /\ g is V45() V46() V47() Element of bool REAL
f | g is Relation-like REAL -defined g -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
dom (f | g) is V45() V46() V47() Element of bool g
((dom A) /\ g) /\ (dom (f | g)) is V45() V46() V47() Element of bool g
dom f is V45() V46() V47() Element of bool REAL
(dom f) /\ g is V45() V46() V47() Element of bool REAL
((dom A) /\ g) /\ ((dom f) /\ g) is V45() V46() V47() Element of bool REAL
g /\ ((dom f) /\ g) is V45() V46() V47() Element of bool REAL
(dom A) /\ (g /\ ((dom f) /\ g)) is V45() V46() V47() Element of bool REAL
g /\ g is V45() V46() V47() Element of bool REAL
(dom f) /\ (g /\ g) is V45() V46() V47() Element of bool REAL
(dom A) /\ ((dom f) /\ (g /\ g)) is V45() V46() V47() Element of bool REAL
(dom A) /\ ((dom f) /\ g) is V45() V46() V47() Element of bool REAL
dom ((A + f),g) is V45() V46() V47() Element of bool g
dom (A + f) is V45() V46() V47() Element of bool REAL
(dom (A + f)) /\ g is V45() V46() V47() Element of bool REAL
(dom A) /\ (dom f) is V45() V46() V47() Element of bool REAL
((dom A) /\ (dom f)) /\ g is V45() V46() V47() Element of bool REAL
X is V22() real ext-real Element of g
((A + f),g) . X is V22() real ext-real Element of REAL
((A,g) + (f,g)) . X is V22() real ext-real Element of REAL
dom (A,g) is V45() V46() V47() Element of bool g
(dom (A,g)) /\ (dom (f,g)) is V45() V46() V47() Element of bool g
(A + f) . X is V22() real ext-real Element of REAL
A . X is V22() real ext-real Element of REAL
f . X is V22() real ext-real Element of REAL
(A . X) + (f . X) is V22() real ext-real Element of REAL
(A | g) . X is V22() real ext-real Element of REAL
(f,g) . X is V22() real ext-real Element of REAL
((A | g) . X) + ((f,g) . X) is V22() real ext-real Element of REAL
(f | g) . X is V22() real ext-real Element of REAL
(A . X) + ((f | g) . X) is V22() real ext-real Element of REAL
A is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(f,A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
[:A,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:A,REAL:] is non empty non trivial V60() set
integral (f,A) is V22() real ext-real Element of REAL
A is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
dom f is V45() V46() V47() Element of bool REAL
(f,A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
[:A,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:A,REAL:] is non empty non trivial V60() set
dom (f,A) is V45() V46() V47() Element of bool A
bool A is set
(dom f) /\ A is V45() V46() V47() Element of bool REAL
A is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(f,A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
[:A,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:A,REAL:] is non empty non trivial V60() set
(f,A) | A is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
dom f is V45() V46() V47() Element of bool REAL
A /\ (dom f) is V45() V46() V47() Element of bool REAL
g is V22() real ext-real set
dom (f,A) is V45() V46() V47() Element of bool A
bool A is set
A /\ (dom (f,A)) is V45() V46() V47() Element of bool A
X is set
(f,A) . X is V22() real ext-real Element of REAL
dom (f | A) is V45() V46() V47() Element of bool A
(dom f) /\ A is V45() V46() V47() Element of bool REAL
f . X is V22() real ext-real Element of REAL
A is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(f,A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
[:A,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:A,REAL:] is non empty non trivial V60() set
(f,A) | A is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
dom f is V45() V46() V47() Element of bool REAL
A /\ (dom f) is V45() V46() V47() Element of bool REAL
g is V22() real ext-real set
dom (f,A) is V45() V46() V47() Element of bool A
bool A is set
A /\ (dom (f,A)) is V45() V46() V47() Element of bool A
X is set
(f,A) . X is V22() real ext-real Element of REAL
dom (f | A) is V45() V46() V47() Element of bool A
(dom f) /\ A is V45() V46() V47() Element of bool REAL
f . X is V22() real ext-real Element of REAL
A is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(f,A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
[:A,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:A,REAL:] is non empty non trivial V60() set
(f,A) | A is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
A is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
dom f is V45() V46() V47() Element of bool REAL
f | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f .: A is V45() V46() V47() Element of bool REAL
g is V22() real ext-real set
X is V22() real ext-real set
X is V22() real ext-real set
a1 is V22() real ext-real set
A /\ (dom f) is V45() V46() V47() Element of bool REAL
a1 is set
f . a1 is V22() real ext-real Element of REAL
a1 is set
f . a1 is V22() real ext-real Element of REAL
A is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
dom f is V45() V46() V47() Element of bool REAL
f | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
[:A,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:A,REAL:] is non empty non trivial V60() set
g is Relation-like A -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
dom g is V45() V46() V47() Element of bool A
bool A is set
(dom f) /\ A is V45() V46() V47() Element of bool REAL
f .: A is V45() V46() V47() Element of bool REAL
rng g is V45() V46() V47() Element of bool REAL
X is set
a1 is set
f . a1 is V22() real ext-real Element of REAL
g . a1 is V22() real ext-real Element of REAL
X is set
a1 is set
g . a1 is V22() real ext-real Element of REAL
f . a1 is V22() real ext-real Element of REAL
g | A is Relation-like A -defined A -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
divs A is non empty set
[:NAT,(divs A):] is Relation-like non empty non trivial V60() set
bool [:NAT,(divs A):] is non empty non trivial V60() set
X is Relation-like A -defined REAL -valued V6() non empty total V30(A, REAL ) V35() V36() V37() Element of bool [:A,REAL:]
a1 is Relation-like NAT -defined divs A -valued V6() non empty total V30( NAT , divs A) Element of bool [:NAT,(divs A):]
delta a1 is Relation-like NAT -defined REAL -valued V6() non empty total V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
lim (delta a1) is V22() real ext-real Element of REAL
upper_sum (X,a1) is Relation-like NAT -defined REAL -valued V6() non empty total V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
lim (upper_sum (X,a1)) is V22() real ext-real Element of REAL
lower_sum (X,a1) is Relation-like NAT -defined REAL -valued V6() non empty total V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
lim (lower_sum (X,a1)) is V22() real ext-real Element of REAL
(lim (upper_sum (X,a1))) - (lim (lower_sum (X,a1))) is V22() real ext-real Element of REAL
(upper_sum (X,a1)) - (lower_sum (X,a1)) is Relation-like NAT -defined REAL -valued V6() non empty total V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
- (lower_sum (X,a1)) is Relation-like NAT -defined V6() total V35() V36() V37() set
- 1 is V22() real ext-real non positive set
(- 1) (#) (lower_sum (X,a1)) is Relation-like NAT -defined V6() total V35() V36() V37() set
(upper_sum (X,a1)) + (- (lower_sum (X,a1))) is Relation-like NAT -defined V6() total V35() V36() V37() set
b1 is Relation-like NAT -defined REAL -valued V6() non empty total V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
x is V22() real ext-real set
vol A is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
x * (vol A) is V22() real ext-real Element of REAL
x / (vol A) is V22() real ext-real Element of REAL
x is V22() real ext-real set
x is V22() real ext-real Element of REAL
x * (vol A) is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
x * (vol A) is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
x * (vol A) is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
x * (vol A) is V22() real ext-real Element of REAL
dom (f | A) is V45() V46() V47() Element of bool A
x is V22() real ext-real Element of REAL
p is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
r2 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
(upper_sum (X,a1)) . r2 is V22() real ext-real Element of REAL
(lower_sum (X,a1)) . r2 is V22() real ext-real Element of REAL
((upper_sum (X,a1)) . r2) - ((lower_sum (X,a1)) . r2) is V22() real ext-real Element of REAL
a1 . r2 is Relation-like NAT -defined REAL -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like Division of A
x is Relation-like NAT -defined REAL -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like Division of A
upper_volume (X,x) is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len (upper_volume (X,x)) is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len x is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len x) -tuples_on REAL is V9() non empty FinSequence-membered FinSequenceSet of REAL
lower_volume (X,x) is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len (lower_volume (X,x)) is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
y is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() V82( len x) FinSequence-like FinSubsequence-like Element of (len x) -tuples_on REAL
LV is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() V82( len x) FinSequence-like FinSubsequence-like Element of (len x) -tuples_on REAL
y - LV is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() V82( len x) FinSequence-like FinSubsequence-like Element of (len x) -tuples_on REAL
- LV is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like set
(- 1) (#) LV is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like set
y + (- LV) is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like set
chi (A,A) is Relation-like A -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
upper_volume ((chi (A,A)),x) is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len (upper_volume ((chi (A,A)),x)) is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom x is non empty V45() V46() V47() V48() V49() V50() V60() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
k is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
(upper_volume (X,x)) . k is V22() real ext-real Element of REAL
(lower_volume (X,x)) . k is V22() real ext-real Element of REAL
((upper_volume (X,x)) . k) - ((lower_volume (X,x)) . k) is V22() real ext-real Element of REAL
(upper_volume ((chi (A,A)),x)) . k is V22() real ext-real Element of REAL
x * ((upper_volume ((chi (A,A)),x)) . k) is V22() real ext-real Element of REAL
divset (x,k) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
[:(divset (x,k)),REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:(divset (x,k)),REAL:] is non empty non trivial V60() set
X | (divset (x,k)) is Relation-like A -defined divset (x,k) -defined A -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
dom X is non empty V45() V46() V47() Element of bool A
(dom X) /\ (divset (x,k)) is V45() V46() V47() Element of bool REAL
h is Relation-like divset (x,k) -defined REAL -valued V6() V35() V36() V37() Element of bool [:(divset (x,k)),REAL:]
dom h is V45() V46() V47() Element of bool (divset (x,k))
bool (divset (x,k)) is set
h is Relation-like divset (x,k) -defined REAL -valued V6() non empty total V30( divset (x,k), REAL ) V35() V36() V37() Element of bool [:(divset (x,k)),REAL:]
vol (divset (x,k)) is V22() real ext-real Element of REAL
Seg (len x) is non empty V45() V46() V47() V48() V49() V50() V60() V82( len x) left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
Seg (len (upper_volume ((chi (A,A)),x))) is non empty V45() V46() V47() V48() V49() V50() V60() V82( len (upper_volume ((chi (A,A)),x))) left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
dom (upper_volume ((chi (A,A)),x)) is non empty V45() V46() V47() V48() V49() V50() V60() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
rng (upper_volume ((chi (A,A)),x)) is non empty V45() V46() V47() V60() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
dom h is non empty V45() V46() V47() Element of bool (divset (x,k))
x1 is V22() real ext-real Element of REAL
h . x1 is V22() real ext-real Element of REAL
x2 is V22() real ext-real Element of REAL
h . x2 is V22() real ext-real Element of REAL
(h . x1) - (h . x2) is V22() real ext-real Element of REAL
abs ((h . x1) - (h . x2)) is V22() real ext-real Element of REAL
X . x2 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
x1 - x2 is V22() real ext-real Element of REAL
abs (x1 - x2) is V22() real ext-real Element of REAL
(delta a1) . r2 is V22() real ext-real Element of REAL
upper_bound (divset (x,k)) is V22() real ext-real Element of REAL
lower_bound (divset (x,k)) is V22() real ext-real Element of REAL
(upper_bound (divset (x,k))) - (lower_bound (divset (x,k))) is V22() real ext-real Element of REAL
sup (rng (upper_volume ((chi (A,A)),x))) is V22() real ext-real set
delta (a1 . r2) is V22() real ext-real Element of REAL
- (x1 - x2) is V22() real ext-real Element of REAL
x2 - x1 is V22() real ext-real Element of REAL
upper_bound (divset (x,k)) is V22() real ext-real Element of REAL
lower_bound (divset (x,k)) is V22() real ext-real Element of REAL
(upper_bound (divset (x,k))) - (lower_bound (divset (x,k))) is V22() real ext-real Element of REAL
sup (rng (upper_volume ((chi (A,A)),x))) is V22() real ext-real set
delta (a1 . r2) is V22() real ext-real Element of REAL
delta x is V22() real ext-real Element of REAL
sup (rng (upper_volume ((chi (A,A)),x))) is V22() real ext-real set
((delta a1) . r2) - 0 is V22() real ext-real Element of REAL
abs (((delta a1) . r2) - 0) is V22() real ext-real Element of REAL
X . x1 is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
vol (divset (x,k)) is V22() real ext-real Element of REAL
rng (X | (divset (x,k))) is V45() V46() V47() Element of bool REAL
upper_bound (rng (X | (divset (x,k)))) is V22() real ext-real Element of REAL
lower_bound (rng (X | (divset (x,k)))) is V22() real ext-real Element of REAL
(upper_bound (rng (X | (divset (x,k))))) - (lower_bound (rng (X | (divset (x,k))))) is V22() real ext-real Element of REAL
((upper_bound (rng (X | (divset (x,k))))) - (lower_bound (rng (X | (divset (x,k)))))) * (vol (divset (x,k))) is V22() real ext-real Element of REAL
x * (vol (divset (x,k))) is V22() real ext-real Element of REAL
(upper_bound (rng (X | (divset (x,k))))) * (vol (divset (x,k))) is V22() real ext-real Element of REAL
(lower_bound (rng (X | (divset (x,k))))) * (vol (divset (x,k))) is V22() real ext-real Element of REAL
((upper_bound (rng (X | (divset (x,k))))) * (vol (divset (x,k)))) - ((lower_bound (rng (X | (divset (x,k))))) * (vol (divset (x,k)))) is V22() real ext-real Element of REAL
((upper_volume (X,x)) . k) - ((lower_bound (rng (X | (divset (x,k))))) * (vol (divset (x,k)))) is V22() real ext-real Element of REAL
Seg (len x) is non empty V45() V46() V47() V48() V49() V50() V60() V82( len x) left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
OSC is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() V82( len x) FinSequence-like FinSubsequence-like Element of (len x) -tuples_on REAL
VOL is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() V82( len x) FinSequence-like FinSubsequence-like Element of (len x) -tuples_on REAL
x * VOL is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() V82( len x) FinSequence-like FinSubsequence-like Element of (len x) -tuples_on REAL
k is ordinal natural V22() real ext-real V60() V80() set
OSC . k is V22() real ext-real Element of REAL
(x * VOL) . k is V22() real ext-real Element of REAL
(upper_volume (X,x)) . k is V22() real ext-real Element of REAL
(lower_volume (X,x)) . k is V22() real ext-real Element of REAL
((upper_volume (X,x)) . k) - ((lower_volume (X,x)) . k) is V22() real ext-real Element of REAL
VOL . k is V22() real ext-real Element of REAL
x * (VOL . k) is V22() real ext-real Element of REAL
Sum OSC is V22() real ext-real Element of REAL
Sum (x * VOL) is V22() real ext-real Element of REAL
Sum VOL is V22() real ext-real Element of REAL
x * (Sum VOL) is V22() real ext-real Element of REAL
Sum y is V22() real ext-real Element of REAL
Sum LV is V22() real ext-real Element of REAL
(Sum y) - (Sum LV) is V22() real ext-real Element of REAL
upper_sum (X,x) is V22() real ext-real Element of REAL
(upper_sum (X,x)) - (Sum LV) is V22() real ext-real Element of REAL
lower_sum (X,x) is V22() real ext-real Element of REAL
(upper_sum (X,x)) - (lower_sum (X,x)) is V22() real ext-real Element of REAL
((upper_sum (X,a1)) . r2) - (lower_sum (X,x)) is V22() real ext-real Element of REAL
r2 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
b1 . r2 is V22() real ext-real Element of REAL
(b1 . r2) - 0 is V22() real ext-real Element of REAL
abs ((b1 . r2) - 0) is V22() real ext-real Element of REAL
a1 . r2 is Relation-like NAT -defined REAL -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like Division of A
(upper_sum (X,a1)) . r2 is V22() real ext-real Element of REAL
(lower_sum (X,a1)) . r2 is V22() real ext-real Element of REAL
((upper_sum (X,a1)) . r2) - ((lower_sum (X,a1)) . r2) is V22() real ext-real Element of REAL
x is Relation-like NAT -defined REAL -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like Division of A
lower_sum (X,x) is V22() real ext-real Element of REAL
upper_sum (X,x) is V22() real ext-real Element of REAL
- (lower_sum (X,a1)) is Relation-like NAT -defined REAL -valued V6() non empty total V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
(- (lower_sum (X,a1))) . r2 is V22() real ext-real Element of REAL
((upper_sum (X,a1)) . r2) + ((- (lower_sum (X,a1))) . r2) is V22() real ext-real Element of REAL
- ((lower_sum (X,a1)) . r2) is V22() real ext-real Element of REAL
((upper_sum (X,a1)) . r2) + (- ((lower_sum (X,a1)) . r2)) is V22() real ext-real Element of REAL
lim b1 is V22() real ext-real Element of REAL
A is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound A is V22() real ext-real Element of REAL
lower_bound A is V22() real ext-real Element of REAL
f is set
g is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
g `| f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(g `| f) | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
((g `| f),A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
[:A,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:A,REAL:] is non empty non trivial V60() set
g . (upper_bound A) is V22() real ext-real Element of REAL
g . (lower_bound A) is V22() real ext-real Element of REAL
(g . (upper_bound A)) - (g . (lower_bound A)) is V22() real ext-real Element of REAL
X is Relation-like NAT -defined REAL -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like Division of A
lower_sum (((g `| f),A),X) is V22() real ext-real Element of REAL
upper_sum (((g `| f),A),X) is V22() real ext-real Element of REAL
len X is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len X) - 1 is V22() real ext-real Element of REAL
a1 is ordinal natural V22() real ext-real V60() V80() set
1 + a1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
b1 is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len b1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
dom b1 is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
dom g is V45() V46() V47() Element of bool REAL
dom X is non empty V45() V46() V47() V48() V49() V50() V60() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
x is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
divset (X,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (X,x)) is V22() real ext-real Element of REAL
g . (upper_bound (divset (X,x))) is V22() real ext-real Element of REAL
lower_bound (divset (X,x)) is V22() real ext-real Element of REAL
g . (lower_bound (divset (X,x))) is V22() real ext-real Element of REAL
(g . (upper_bound (divset (X,x)))) - (g . (lower_bound (divset (X,x)))) is V22() real ext-real Element of REAL
vol (divset (X,x)) is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
(upper_bound (divset (X,x))) - (lower_bound (divset (X,x))) is V22() real ext-real Element of REAL
diff (g,x) is V22() real ext-real Element of REAL
(diff (g,x)) * (vol (divset (X,x))) is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
g | f is Relation-like REAL -defined f -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
g | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
g | (divset (X,x)) is Relation-like REAL -defined divset (X,x) -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
[.(lower_bound (divset (X,x))),(upper_bound (divset (X,x))).] is V45() V46() V47() closed interval Element of bool REAL
].(lower_bound (divset (X,x))),(upper_bound (divset (X,x))).[ is V45() V46() V47() open non left_end non right_end interval Element of bool REAL
(upper_bound (divset (X,x))) - (lower_bound (divset (X,x))) is V22() real ext-real Element of REAL
((g . (upper_bound (divset (X,x)))) - (g . (lower_bound (divset (X,x))))) / ((upper_bound (divset (X,x))) - (lower_bound (divset (X,x)))) is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
diff (g,x) is V22() real ext-real Element of REAL
(diff (g,x)) * ((upper_bound (divset (X,x))) - (lower_bound (divset (X,x)))) is V22() real ext-real Element of REAL
(diff (g,x)) * (vol (divset (X,x))) is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
diff (g,x) is V22() real ext-real Element of REAL
(diff (g,x)) * (vol (divset (X,x))) is V22() real ext-real Element of REAL
Seg (len X) is non empty V45() V46() V47() V48() V49() V50() V60() V82( len X) left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
a1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
Seg a1 is V45() V46() V47() V48() V49() V50() V60() V82(a1) bounded_below bounded_above real-bounded Element of bool NAT
x is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
divset (X,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (X,x)) is V22() real ext-real Element of REAL
x + 1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
divset (X,(x + 1)) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
lower_bound (divset (X,(x + 1))) is V22() real ext-real Element of REAL
a1 + 1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
1 + 0 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(x + 1) - 1 is V22() real ext-real Element of REAL
X . x is V22() real ext-real Element of REAL
1 + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
X . x is V22() real ext-real Element of REAL
x is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len x is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
dom x is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
dom (g `| f) is V45() V46() V47() Element of bool REAL
[:f,REAL:] is Relation-like V35() V36() V37() set
bool [:f,REAL:] is set
x is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
divset (X,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
((g `| f),A) | (divset (X,x)) is Relation-like A -defined divset (X,x) -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
rng (((g `| f),A) | (divset (X,x))) is V45() V46() V47() Element of bool REAL
A /\ (dom (g `| f)) is V45() V46() V47() Element of bool REAL
p is V22() real ext-real set
r2 is V22() real ext-real set
dom ((g `| f) | A) is V45() V46() V47() Element of bool A
bool A is set
(dom (g `| f)) /\ A is V45() V46() V47() Element of bool REAL
dom ((g `| f),A) is V45() V46() V47() Element of bool A
A /\ (dom ((g `| f),A)) is V45() V46() V47() Element of bool A
x is set
((g `| f),A) . x is V22() real ext-real Element of REAL
A /\ (A /\ (dom (g `| f))) is V45() V46() V47() Element of bool REAL
A /\ A is V45() V46() V47() interval Element of bool REAL
(A /\ A) /\ (dom (g `| f)) is V45() V46() V47() Element of bool REAL
x is Relation-like f -defined REAL -valued V6() V35() V36() V37() Element of bool [:f,REAL:]
x . x is V22() real ext-real Element of REAL
y is V22() real ext-real Element of REAL
((g `| f),A) | A is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
x is set
((g `| f),A) . x is V22() real ext-real Element of REAL
A /\ (A /\ (dom (g `| f))) is V45() V46() V47() Element of bool REAL
A /\ A is V45() V46() V47() interval Element of bool REAL
(A /\ A) /\ (dom (g `| f)) is V45() V46() V47() Element of bool REAL
x is Relation-like f -defined REAL -valued V6() V35() V36() V37() Element of bool [:f,REAL:]
x . x is V22() real ext-real Element of REAL
y is V22() real ext-real Element of REAL
x is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len x is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
dom x is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
<*(g . (upper_bound A))*> is Relation-like NAT -defined REAL -valued V6() V7() non empty trivial V35() V36() V37() increasing decreasing non-decreasing non-increasing V60() V82(1) FinSequence-like FinSubsequence-like FinSequence of REAL
x ^ <*(g . (upper_bound A))*> is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len (x ^ <*(g . (upper_bound A))*>) is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
<*(g . (lower_bound A))*> is Relation-like NAT -defined REAL -valued V6() V7() non empty trivial V35() V36() V37() increasing decreasing non-decreasing non-increasing V60() V82(1) FinSequence-like FinSubsequence-like FinSequence of REAL
<*(g . (lower_bound A))*> ^ x is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len (<*(g . (lower_bound A))*> ^ x) is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom (x ^ <*(g . (upper_bound A))*>) is non empty V45() V46() V47() V48() V49() V50() V60() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
dom <*(g . (upper_bound A))*> is non empty trivial V45() V46() V47() V48() V49() V50() V60() V82(1) left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
len <*(g . (upper_bound A))*> is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
a1 + 1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
dom <*(g . (lower_bound A))*> is non empty trivial V45() V46() V47() V48() V49() V50() V60() V82(1) left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
len <*(g . (lower_bound A))*> is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
x is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
b1 . x is V22() real ext-real Element of REAL
(x ^ <*(g . (upper_bound A))*>) /. x is V22() real ext-real Element of REAL
(<*(g . (lower_bound A))*> ^ x) /. x is V22() real ext-real Element of REAL
((x ^ <*(g . (upper_bound A))*>) /. x) - ((<*(g . (lower_bound A))*> ^ x) /. x) is V22() real ext-real Element of REAL
(x ^ <*(g . (upper_bound A))*>) . x is V22() real ext-real Element of REAL
Seg (len (x ^ <*(g . (upper_bound A))*>)) is non empty V45() V46() V47() V48() V49() V50() V60() V82( len (x ^ <*(g . (upper_bound A))*>)) left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
dom (<*(g . (lower_bound A))*> ^ x) is non empty V45() V46() V47() V48() V49() V50() V60() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
(<*(g . (lower_bound A))*> ^ x) . x is V22() real ext-real Element of REAL
X . x is V22() real ext-real Element of REAL
divset (X,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (X,x)) is V22() real ext-real Element of REAL
g . (upper_bound (divset (X,x))) is V22() real ext-real Element of REAL
lower_bound (divset (X,x)) is V22() real ext-real Element of REAL
g . (lower_bound (divset (X,x))) is V22() real ext-real Element of REAL
(g . (upper_bound (divset (X,x)))) - (g . (lower_bound (divset (X,x)))) is V22() real ext-real Element of REAL
2 - 1 is V22() real ext-real Element of REAL
<*(g . (lower_bound A))*> . x is V22() real ext-real Element of REAL
x . x is V22() real ext-real Element of REAL
divset (X,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (X,x)) is V22() real ext-real Element of REAL
g . (upper_bound (divset (X,x))) is V22() real ext-real Element of REAL
lower_bound (divset (X,x)) is V22() real ext-real Element of REAL
g . (lower_bound (divset (X,x))) is V22() real ext-real Element of REAL
(g . (upper_bound (divset (X,x)))) - (g . (lower_bound (divset (X,x)))) is V22() real ext-real Element of REAL
x - (len x) is V22() real ext-real Element of REAL
(x - (len x)) + (len x) is V22() real ext-real Element of REAL
<*(g . (upper_bound A))*> . (x - (len x)) is V22() real ext-real Element of REAL
x - (len <*(g . (lower_bound A))*>) is V22() real ext-real Element of REAL
x - 1 is V22() real ext-real Element of REAL
divset (X,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (X,x)) is V22() real ext-real Element of REAL
g . (upper_bound (divset (X,x))) is V22() real ext-real Element of REAL
lower_bound (divset (X,x)) is V22() real ext-real Element of REAL
g . (lower_bound (divset (X,x))) is V22() real ext-real Element of REAL
(g . (upper_bound (divset (X,x)))) - (g . (lower_bound (divset (X,x)))) is V22() real ext-real Element of REAL
X . (x - 1) is V22() real ext-real Element of REAL
g . (X . (x - 1)) is V22() real ext-real Element of REAL
(g . (upper_bound (divset (X,x)))) - (g . (X . (x - 1))) is V22() real ext-real Element of REAL
X . x is V22() real ext-real Element of REAL
g . (X . x) is V22() real ext-real Element of REAL
(g . (X . x)) - (g . (X . (x - 1))) is V22() real ext-real Element of REAL
(len <*(g . (lower_bound A))*>) + (x - (len <*(g . (lower_bound A))*>)) is V22() real ext-real Element of REAL
x . (x - (len <*(g . (lower_bound A))*>)) is V22() real ext-real Element of REAL
(len x) + (len <*(g . (upper_bound A))*>) is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
x - 1 is V22() real ext-real Element of REAL
(x - 1) + 1 is V22() real ext-real Element of REAL
x - (len <*(g . (lower_bound A))*>) is V22() real ext-real Element of REAL
1 + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len x) is V45() V46() V47() V48() V49() V50() V60() V82( len x) bounded_below bounded_above real-bounded Element of bool NAT
a1 - 1 is V22() real ext-real Element of REAL
(x - 1) + 0 is V22() real ext-real Element of REAL
(a1 - 1) + 1 is V22() real ext-real Element of REAL
p is ordinal natural V22() real ext-real V60() V80() set
1 + p is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
Seg (len x) is V45() V46() V47() V48() V49() V50() V60() V82( len x) bounded_below bounded_above real-bounded Element of bool NAT
Seg (len x) is V45() V46() V47() V48() V49() V50() V60() V82( len x) bounded_below bounded_above real-bounded Element of bool NAT
(len <*(g . (lower_bound A))*>) + (len x) is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
(len <*(g . (lower_bound A))*>) + 1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
x . (x - (len <*(g . (lower_bound A))*>)) is V22() real ext-real Element of REAL
x . (x - 1) is V22() real ext-real Element of REAL
divset (X,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
lower_bound (divset (X,x)) is V22() real ext-real Element of REAL
g . (lower_bound (divset (X,x))) is V22() real ext-real Element of REAL
x . x is V22() real ext-real Element of REAL
upper_bound (divset (X,x)) is V22() real ext-real Element of REAL
g . (upper_bound (divset (X,x))) is V22() real ext-real Element of REAL
Sum b1 is V22() real ext-real Element of REAL
Sum (x ^ <*(g . (upper_bound A))*>) is V22() real ext-real Element of REAL
Sum (<*(g . (lower_bound A))*> ^ x) is V22() real ext-real Element of REAL
(Sum (x ^ <*(g . (upper_bound A))*>)) - (Sum (<*(g . (lower_bound A))*> ^ x)) is V22() real ext-real Element of REAL
Sum x is V22() real ext-real Element of REAL
(Sum x) + (g . (upper_bound A)) is V22() real ext-real Element of REAL
((Sum x) + (g . (upper_bound A))) - (Sum (<*(g . (lower_bound A))*> ^ x)) is V22() real ext-real Element of REAL
Sum x is V22() real ext-real Element of REAL
(g . (lower_bound A)) + (Sum x) is V22() real ext-real Element of REAL
((Sum x) + (g . (upper_bound A))) - ((g . (lower_bound A)) + (Sum x)) is V22() real ext-real Element of REAL
x is ordinal natural V22() real ext-real V60() V80() set
x . x is V22() real ext-real Element of REAL
x . x is V22() real ext-real Element of REAL
divset (X,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (X,x)) is V22() real ext-real Element of REAL
g . (upper_bound (divset (X,x))) is V22() real ext-real Element of REAL
x + 1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
divset (X,(x + 1)) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
lower_bound (divset (X,(x + 1))) is V22() real ext-real Element of REAL
g . (lower_bound (divset (X,(x + 1)))) is V22() real ext-real Element of REAL
dom ((g `| f) | A) is V45() V46() V47() Element of bool A
bool A is set
dom (g `| f) is V45() V46() V47() Element of bool REAL
(dom (g `| f)) /\ A is V45() V46() V47() Element of bool REAL
f /\ A is V45() V46() V47() Element of bool REAL
x is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
divset (X,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
((g `| f),A) | (divset (X,x)) is Relation-like A -defined divset (X,x) -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
rng (((g `| f),A) | (divset (X,x))) is V45() V46() V47() Element of bool REAL
p is V22() real ext-real Element of REAL
diff (g,p) is V22() real ext-real Element of REAL
(g `| f) . p is V22() real ext-real Element of REAL
((g `| f),A) . p is V22() real ext-real Element of REAL
dom (((g `| f),A) | (divset (X,x))) is V45() V46() V47() Element of bool A
A /\ (divset (X,x)) is V45() V46() V47() interval Element of bool REAL
(((g `| f),A) | (divset (X,x))) . p is V22() real ext-real Element of REAL
upper_volume (((g `| f),A),X) is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
x is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
divset (X,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (X,x)) is V22() real ext-real Element of REAL
g . (upper_bound (divset (X,x))) is V22() real ext-real Element of REAL
lower_bound (divset (X,x)) is V22() real ext-real Element of REAL
g . (lower_bound (divset (X,x))) is V22() real ext-real Element of REAL
(g . (upper_bound (divset (X,x)))) - (g . (lower_bound (divset (X,x)))) is V22() real ext-real Element of REAL
(upper_volume (((g `| f),A),X)) . x is V22() real ext-real Element of REAL
vol (divset (X,x)) is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
diff (g,p) is V22() real ext-real Element of REAL
(diff (g,p)) * (vol (divset (X,x))) is V22() real ext-real Element of REAL
((g `| f),A) | (divset (X,x)) is Relation-like A -defined divset (X,x) -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
rng (((g `| f),A) | (divset (X,x))) is V45() V46() V47() Element of bool REAL
upper_bound (rng (((g `| f),A) | (divset (X,x)))) is V22() real ext-real Element of REAL
(upper_bound (rng (((g `| f),A) | (divset (X,x))))) * (vol (divset (X,x))) is V22() real ext-real Element of REAL
len (upper_volume (((g `| f),A),X)) is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len X) -tuples_on REAL is V9() non empty FinSequence-membered FinSequenceSet of REAL
p is ordinal natural V22() real ext-real V60() V80() set
b1 . p is V22() real ext-real Element of REAL
(upper_volume (((g `| f),A),X)) . p is V22() real ext-real Element of REAL
divset (X,p) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (X,p)) is V22() real ext-real Element of REAL
g . (upper_bound (divset (X,p))) is V22() real ext-real Element of REAL
lower_bound (divset (X,p)) is V22() real ext-real Element of REAL
g . (lower_bound (divset (X,p))) is V22() real ext-real Element of REAL
(g . (upper_bound (divset (X,p)))) - (g . (lower_bound (divset (X,p)))) is V22() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() V82( len X) FinSequence-like FinSubsequence-like Element of (len X) -tuples_on REAL
Sum p is V22() real ext-real Element of REAL
x is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() V82( len X) FinSequence-like FinSubsequence-like Element of (len X) -tuples_on REAL
Sum x is V22() real ext-real Element of REAL
lower_volume (((g `| f),A),X) is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
x is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
(lower_volume (((g `| f),A),X)) . x is V22() real ext-real Element of REAL
divset (X,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (X,x)) is V22() real ext-real Element of REAL
g . (upper_bound (divset (X,x))) is V22() real ext-real Element of REAL
lower_bound (divset (X,x)) is V22() real ext-real Element of REAL
g . (lower_bound (divset (X,x))) is V22() real ext-real Element of REAL
(g . (upper_bound (divset (X,x)))) - (g . (lower_bound (divset (X,x)))) is V22() real ext-real Element of REAL
vol (divset (X,x)) is V22() real ext-real Element of REAL
((g `| f),A) | (divset (X,x)) is Relation-like A -defined divset (X,x) -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
rng (((g `| f),A) | (divset (X,x))) is V45() V46() V47() Element of bool REAL
lower_bound (rng (((g `| f),A) | (divset (X,x)))) is V22() real ext-real Element of REAL
(lower_bound (rng (((g `| f),A) | (divset (X,x))))) * (vol (divset (X,x))) is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
diff (g,p) is V22() real ext-real Element of REAL
(diff (g,p)) * (vol (divset (X,x))) is V22() real ext-real Element of REAL
len (lower_volume (((g `| f),A),X)) is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len X) -tuples_on REAL is V9() non empty FinSequence-membered FinSequenceSet of REAL
p is ordinal natural V22() real ext-real V60() V80() set
(lower_volume (((g `| f),A),X)) . p is V22() real ext-real Element of REAL
b1 . p is V22() real ext-real Element of REAL
divset (X,p) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (X,p)) is V22() real ext-real Element of REAL
g . (upper_bound (divset (X,p))) is V22() real ext-real Element of REAL
lower_bound (divset (X,p)) is V22() real ext-real Element of REAL
g . (lower_bound (divset (X,p))) is V22() real ext-real Element of REAL
(g . (upper_bound (divset (X,p)))) - (g . (lower_bound (divset (X,p)))) is V22() real ext-real Element of REAL
x is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() V82( len X) FinSequence-like FinSubsequence-like Element of (len X) -tuples_on REAL
Sum x is V22() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() V82( len X) FinSequence-like FinSubsequence-like Element of (len X) -tuples_on REAL
Sum p is V22() real ext-real Element of REAL
A is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound A is V22() real ext-real Element of REAL
lower_bound A is V22() real ext-real Element of REAL
f is set
g is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
g `| f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(g `| f) | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(A,(g `| f)) is V22() real ext-real Element of REAL
((g `| f),A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
[:A,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:A,REAL:] is non empty non trivial V60() set
integral ((g `| f),A) is V22() real ext-real Element of REAL
g . (upper_bound A) is V22() real ext-real Element of REAL
g . (lower_bound A) is V22() real ext-real Element of REAL
(g . (upper_bound A)) - (g . (lower_bound A)) is V22() real ext-real Element of REAL
upper_integral ((g `| f),A) is V22() real ext-real Element of REAL
lower_integral ((g `| f),A) is V22() real ext-real Element of REAL
upper_sum_set ((g `| f),A) is Relation-like divs A -defined REAL -valued V6() non empty total V30( divs A, REAL ) V35() V36() V37() Element of bool [:(divs A),REAL:]
divs A is non empty set
[:(divs A),REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:(divs A),REAL:] is non empty non trivial V60() set
rng (upper_sum_set ((g `| f),A)) is non empty V45() V46() V47() Element of bool REAL
X is V22() real ext-real set
dom (upper_sum_set ((g `| f),A)) is non empty Element of bool (divs A)
bool (divs A) is set
a1 is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like Element of divs A
(upper_sum_set ((g `| f),A)) . a1 is V22() real ext-real Element of REAL
b1 is Relation-like NAT -defined REAL -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like Division of A
upper_sum (((g `| f),A),b1) is V22() real ext-real Element of REAL
lower_bound (rng (upper_sum_set ((g `| f),A))) is V22() real ext-real Element of REAL
lower_sum_set ((g `| f),A) is Relation-like divs A -defined REAL -valued V6() non empty total V30( divs A, REAL ) V35() V36() V37() Element of bool [:(divs A),REAL:]
rng (lower_sum_set ((g `| f),A)) is non empty V45() V46() V47() Element of bool REAL
X is V22() real ext-real set
dom (lower_sum_set ((g `| f),A)) is non empty Element of bool (divs A)
bool (divs A) is set
a1 is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like Element of divs A
(lower_sum_set ((g `| f),A)) . a1 is V22() real ext-real Element of REAL
b1 is Relation-like NAT -defined REAL -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like Division of A
lower_sum (((g `| f),A),b1) is V22() real ext-real Element of REAL
upper_bound (rng (lower_sum_set ((g `| f),A))) is V22() real ext-real Element of REAL
A is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
dom f is V45() V46() V47() Element of bool REAL
rng (f | A) is V45() V46() V47() Element of bool REAL
dom (f | A) is V45() V46() V47() Element of bool A
bool A is set
(dom f) /\ A is V45() V46() V47() Element of bool REAL
lower_bound A is V22() real ext-real Element of REAL
f . (lower_bound A) is V22() real ext-real Element of REAL
upper_bound A is V22() real ext-real Element of REAL
g is ext-real set
X is V22() real ext-real Element of REAL
(f | A) . X is V22() real ext-real Element of REAL
f . X is V22() real ext-real Element of REAL
upper_bound A is V22() real ext-real Element of REAL
f . (upper_bound A) is V22() real ext-real Element of REAL
g is ext-real set
X is V22() real ext-real Element of REAL
(f | A) . X is V22() real ext-real Element of REAL
f . X is V22() real ext-real Element of REAL
A is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
lower_bound A is V22() real ext-real Element of REAL
upper_bound A is V22() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
dom f is V45() V46() V47() Element of bool REAL
rng (f | A) is V45() V46() V47() Element of bool REAL
lower_bound (rng (f | A)) is V22() real ext-real Element of REAL
f . (lower_bound A) is V22() real ext-real Element of REAL
upper_bound (rng (f | A)) is V22() real ext-real Element of REAL
f . (upper_bound A) is V22() real ext-real Element of REAL
dom (f | A) is V45() V46() V47() Element of bool A
bool A is set
(dom f) /\ A is V45() V46() V47() Element of bool REAL
g is V22() real ext-real set
X is V22() real ext-real Element of REAL
(f | A) . X is V22() real ext-real Element of REAL
f . X is V22() real ext-real Element of REAL
g is V22() real ext-real set
X is V22() real ext-real Element of REAL
(f | A) . X is V22() real ext-real Element of REAL
f . X is V22() real ext-real Element of REAL
g is V22() real ext-real set
(f | A) . (lower_bound A) is V22() real ext-real Element of REAL
g is V22() real ext-real set
(f | A) . (upper_bound A) is V22() real ext-real Element of REAL
A is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
dom f is V45() V46() V47() Element of bool REAL
(f,A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
[:A,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:A,REAL:] is non empty non trivial V60() set
g is Relation-like NAT -defined REAL -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like Division of A
dom g is non empty V45() V46() V47() V48() V49() V50() V60() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
upper_volume ((f,A),g) is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
lower_volume ((f,A),g) is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
delta g is V22() real ext-real Element of REAL
X is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
(upper_volume ((f,A),g)) . X is V22() real ext-real Element of REAL
(lower_volume ((f,A),g)) . X is V22() real ext-real Element of REAL
((upper_volume ((f,A),g)) . X) - ((lower_volume ((f,A),g)) . X) is V22() real ext-real Element of REAL
divset (g,X) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (g,X)) is V22() real ext-real Element of REAL
f . (upper_bound (divset (g,X))) is V22() real ext-real Element of REAL
lower_bound (divset (g,X)) is V22() real ext-real Element of REAL
f . (lower_bound (divset (g,X))) is V22() real ext-real Element of REAL
(f . (upper_bound (divset (g,X)))) - (f . (lower_bound (divset (g,X)))) is V22() real ext-real Element of REAL
((f . (upper_bound (divset (g,X)))) - (f . (lower_bound (divset (g,X))))) * (delta g) is V22() real ext-real Element of REAL
(f,A) | (divset (g,X)) is Relation-like A -defined divset (g,X) -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
rng ((f,A) | (divset (g,X))) is V45() V46() V47() Element of bool REAL
upper_bound (rng ((f,A) | (divset (g,X)))) is V22() real ext-real Element of REAL
vol (divset (g,X)) is V22() real ext-real Element of REAL
(upper_bound (rng ((f,A) | (divset (g,X))))) * (vol (divset (g,X))) is V22() real ext-real Element of REAL
lower_bound (rng ((f,A) | (divset (g,X)))) is V22() real ext-real Element of REAL
(lower_bound (rng ((f,A) | (divset (g,X))))) * (vol (divset (g,X))) is V22() real ext-real Element of REAL
len g is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len g) is non empty V45() V46() V47() V48() V49() V50() V60() V82( len g) left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
chi (A,A) is Relation-like A -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
upper_volume ((chi (A,A)),g) is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len (upper_volume ((chi (A,A)),g)) is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len (upper_volume ((chi (A,A)),g))) is non empty V45() V46() V47() V48() V49() V50() V60() V82( len (upper_volume ((chi (A,A)),g))) left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
dom (upper_volume ((chi (A,A)),g)) is non empty V45() V46() V47() V48() V49() V50() V60() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
(upper_volume ((chi (A,A)),g)) . X is V22() real ext-real Element of REAL
rng (upper_volume ((chi (A,A)),g)) is non empty V45() V46() V47() V60() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
sup (rng (upper_volume ((chi (A,A)),g))) is V22() real ext-real set
f | (divset (g,X)) is Relation-like REAL -defined divset (g,X) -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
rng (f | (divset (g,X))) is V45() V46() V47() Element of bool REAL
lower_bound (rng (f | (divset (g,X)))) is V22() real ext-real Element of REAL
upper_bound (rng (f | (divset (g,X)))) is V22() real ext-real Element of REAL
dom (f | (divset (g,X))) is V45() V46() V47() Element of bool REAL
(dom f) /\ (divset (g,X)) is V45() V46() V47() Element of bool REAL
rng (f | A) is V45() V46() V47() Element of bool REAL
0 * (vol (divset (g,X))) is V22() real ext-real Element of REAL
((f . (upper_bound (divset (g,X)))) - (f . (lower_bound (divset (g,X))))) * (vol (divset (g,X))) is V22() real ext-real Element of REAL
upper_bound A is V22() real ext-real Element of REAL
f . (upper_bound A) is V22() real ext-real Element of REAL
lower_bound A is V22() real ext-real Element of REAL
f . (lower_bound A) is V22() real ext-real Element of REAL
(f . (upper_bound A)) - (f . (lower_bound A)) is V22() real ext-real Element of REAL
g is Relation-like NAT -defined REAL -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like Division of A
upper_sum ((f,A),g) is V22() real ext-real Element of REAL
lower_sum ((f,A),g) is V22() real ext-real Element of REAL
(upper_sum ((f,A),g)) - (lower_sum ((f,A),g)) is V22() real ext-real Element of REAL
delta g is V22() real ext-real Element of REAL
(delta g) * ((f . (upper_bound A)) - (f . (lower_bound A))) is V22() real ext-real Element of REAL
len g is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
X is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len X is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
dom X is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
(len g) - 1 is V22() real ext-real Element of REAL
a1 is ordinal natural V22() real ext-real V60() V80() set
1 + a1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
a1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
b1 is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len b1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
dom b1 is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
Seg (len g) is non empty V45() V46() V47() V48() V49() V50() V60() V82( len g) left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
x is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len x is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
dom x is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
Seg a1 is V45() V46() V47() V48() V49() V50() V60() V82(a1) bounded_below bounded_above real-bounded Element of bool NAT
<*(f . (lower_bound A))*> is Relation-like NAT -defined REAL -valued V6() V7() non empty trivial V35() V36() V37() increasing decreasing non-decreasing non-increasing V60() V82(1) FinSequence-like FinSubsequence-like FinSequence of REAL
<*(f . (lower_bound A))*> ^ x is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
x is ordinal natural V22() real ext-real V60() V80() set
b1 . x is V22() real ext-real Element of REAL
(<*(f . (lower_bound A))*> ^ x) . x is V22() real ext-real Element of REAL
dom g is non empty V45() V46() V47() V48() V49() V50() V60() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
divset (g,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
lower_bound (divset (g,x)) is V22() real ext-real Element of REAL
f . (lower_bound (divset (g,x))) is V22() real ext-real Element of REAL
1 + 1 is non empty ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len <*(f . (lower_bound A))*> is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len <*(f . (lower_bound A))*>) + 1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
dom g is non empty V45() V46() V47() V48() V49() V50() V60() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
x - 1 is V22() real ext-real Element of REAL
x is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
x + 1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
divset (g,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (g,x)) is V22() real ext-real Element of REAL
g . (x - 1) is V22() real ext-real Element of REAL
(len g) + 1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
1 + ((len g) - 1) is V22() real ext-real Element of REAL
(len <*(f . (lower_bound A))*>) + (len x) is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
x - (len <*(f . (lower_bound A))*>) is V22() real ext-real Element of REAL
x . (x - (len <*(f . (lower_bound A))*>)) is V22() real ext-real Element of REAL
x . (x - 1) is V22() real ext-real Element of REAL
divset (g,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
lower_bound (divset (g,x)) is V22() real ext-real Element of REAL
f . (lower_bound (divset (g,x))) is V22() real ext-real Element of REAL
f . (g . (x - 1)) is V22() real ext-real Element of REAL
len (<*(f . (lower_bound A))*> ^ x) is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len <*(f . (lower_bound A))*> is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len <*(f . (lower_bound A))*>) + (len x) is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
1 + ((len g) - 1) is V22() real ext-real Element of REAL
upper_volume ((f,A),g) is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len (upper_volume ((f,A),g)) is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
lower_volume ((f,A),g) is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
len (lower_volume ((f,A),g)) is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(upper_volume ((f,A),g)) - (lower_volume ((f,A),g)) is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
- (lower_volume ((f,A),g)) is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like set
- 1 is V22() real ext-real non positive set
(- 1) (#) (lower_volume ((f,A),g)) is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like set
(upper_volume ((f,A),g)) + (- (lower_volume ((f,A),g))) is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like set
Sum ((upper_volume ((f,A),g)) - (lower_volume ((f,A),g))) is V22() real ext-real Element of REAL
Sum (upper_volume ((f,A),g)) is V22() real ext-real Element of REAL
Sum (lower_volume ((f,A),g)) is V22() real ext-real Element of REAL
(Sum (upper_volume ((f,A),g))) - (Sum (lower_volume ((f,A),g))) is V22() real ext-real Element of REAL
(upper_sum ((f,A),g)) - (Sum (lower_volume ((f,A),g))) is V22() real ext-real Element of REAL
<*(f . (upper_bound A))*> is Relation-like NAT -defined REAL -valued V6() V7() non empty trivial V35() V36() V37() increasing decreasing non-decreasing non-increasing V60() V82(1) FinSequence-like FinSubsequence-like FinSequence of REAL
x ^ <*(f . (upper_bound A))*> is Relation-like NAT -defined REAL -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
x is ordinal natural V22() real ext-real V60() V80() set
X . x is V22() real ext-real Element of REAL
(x ^ <*(f . (upper_bound A))*>) . x is V22() real ext-real Element of REAL
Seg (len x) is V45() V46() V47() V48() V49() V50() V60() V82( len x) bounded_below bounded_above real-bounded Element of bool NAT
x . x is V22() real ext-real Element of REAL
divset (g,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (g,x)) is V22() real ext-real Element of REAL
f . (upper_bound (divset (g,x))) is V22() real ext-real Element of REAL
Seg (len X) is V45() V46() V47() V48() V49() V50() V60() V82( len X) bounded_below bounded_above real-bounded Element of bool NAT
(len x) + 1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
Seg (len X) is V45() V46() V47() V48() V49() V50() V60() V82( len X) bounded_below bounded_above real-bounded Element of bool NAT
dom g is non empty V45() V46() V47() V48() V49() V50() V60() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
divset (g,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (g,x)) is V22() real ext-real Element of REAL
g . x is V22() real ext-real Element of REAL
f . (upper_bound (divset (g,x))) is V22() real ext-real Element of REAL
g . (len g) is V22() real ext-real Element of REAL
f . (g . (len g)) is V22() real ext-real Element of REAL
len ((upper_volume ((f,A),g)) - (lower_volume ((f,A),g))) is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
X - b1 is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
- b1 is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like set
(- 1) (#) b1 is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like set
X + (- b1) is Relation-like NAT -defined V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like set
len (X - b1) is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
dom ((upper_volume ((f,A),g)) - (lower_volume ((f,A),g))) is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
(delta g) * (X - b1) is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like FinSequence of REAL
x is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
((upper_volume ((f,A),g)) - (lower_volume ((f,A),g))) . x is V22() real ext-real Element of REAL
((delta g) * (X - b1)) . x is V22() real ext-real Element of REAL
Seg (len (X - b1)) is V45() V46() V47() V48() V49() V50() V60() V82( len (X - b1)) bounded_below bounded_above real-bounded Element of bool NAT
dom (X - b1) is V45() V46() V47() V48() V49() V50() V60() bounded_below bounded_above real-bounded Element of bool NAT
dom g is non empty V45() V46() V47() V48() V49() V50() V60() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
(upper_volume ((f,A),g)) . x is V22() real ext-real Element of REAL
(lower_volume ((f,A),g)) . x is V22() real ext-real Element of REAL
((upper_volume ((f,A),g)) . x) - ((lower_volume ((f,A),g)) . x) is V22() real ext-real Element of REAL
divset (g,x) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (g,x)) is V22() real ext-real Element of REAL
f . (upper_bound (divset (g,x))) is V22() real ext-real Element of REAL
lower_bound (divset (g,x)) is V22() real ext-real Element of REAL
f . (lower_bound (divset (g,x))) is V22() real ext-real Element of REAL
(f . (upper_bound (divset (g,x)))) - (f . (lower_bound (divset (g,x)))) is V22() real ext-real Element of REAL
((f . (upper_bound (divset (g,x)))) - (f . (lower_bound (divset (g,x))))) * (delta g) is V22() real ext-real Element of REAL
X . x is V22() real ext-real Element of REAL
b1 . x is V22() real ext-real Element of REAL
(X - b1) . x is V22() real ext-real Element of REAL
(delta g) * ((X - b1) . x) is V22() real ext-real Element of REAL
(delta g) multreal is Relation-like REAL -defined REAL -valued V6() non empty total V30( REAL , REAL ) V35() V36() V37() Element of bool [:REAL,REAL:]
((delta g) multreal) * (X - b1) is Relation-like NAT -defined REAL -valued V6() V35() V36() V37() V60() Element of bool [:NAT,REAL:]
len ((delta g) * (X - b1)) is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
Sum ((delta g) * (X - b1)) is V22() real ext-real Element of REAL
len (x ^ <*(f . (upper_bound A))*>) is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len <*(f . (upper_bound A))*> is non empty ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len x) + (len <*(f . (upper_bound A))*>) is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
((len g) - 1) + 1 is V22() real ext-real Element of REAL
Sum (X - b1) is V22() real ext-real Element of REAL
x is ordinal natural V22() real ext-real V60() V80() set
((upper_volume ((f,A),g)) - (lower_volume ((f,A),g))) . x is V22() real ext-real Element of REAL
Seg (len ((upper_volume ((f,A),g)) - (lower_volume ((f,A),g)))) is V45() V46() V47() V48() V49() V50() V60() V82( len ((upper_volume ((f,A),g)) - (lower_volume ((f,A),g)))) bounded_below bounded_above real-bounded Element of bool NAT
dom g is non empty V45() V46() V47() V48() V49() V50() V60() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
(upper_volume ((f,A),g)) . x is V22() real ext-real Element of REAL
(lower_volume ((f,A),g)) . x is V22() real ext-real Element of REAL
((upper_volume ((f,A),g)) . x) - ((lower_volume ((f,A),g)) . x) is V22() real ext-real Element of REAL
(f,A) | A is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
g is V22() real ext-real Element of REAL
dom (f,A) is V45() V46() V47() Element of bool A
bool A is set
(dom f) /\ A is V45() V46() V47() Element of bool REAL
A /\ (dom (f,A)) is V45() V46() V47() Element of bool A
(f,A) . (lower_bound A) is V22() real ext-real Element of REAL
A /\ (dom f) is V45() V46() V47() Element of bool REAL
(f | A) . (lower_bound A) is V22() real ext-real Element of REAL
X is set
(f,A) . X is V22() real ext-real Element of REAL
a1 is V22() real ext-real Element of A
f . a1 is V22() real ext-real Element of REAL
(f | A) . a1 is V22() real ext-real Element of REAL
(f,A) . (upper_bound A) is V22() real ext-real Element of REAL
A /\ (dom f) is V45() V46() V47() Element of bool REAL
(f | A) . (upper_bound A) is V22() real ext-real Element of REAL
X is set
(f,A) . X is V22() real ext-real Element of REAL
a1 is V22() real ext-real Element of A
f . a1 is V22() real ext-real Element of REAL
(f | A) . a1 is V22() real ext-real Element of REAL
divs A is non empty set
[:NAT,(divs A):] is Relation-like non empty non trivial V60() set
bool [:NAT,(divs A):] is non empty non trivial V60() set
g is Relation-like NAT -defined divs A -valued V6() non empty total V30( NAT , divs A) Element of bool [:NAT,(divs A):]
delta g is Relation-like NAT -defined REAL -valued V6() non empty total V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
lim (delta g) is V22() real ext-real Element of REAL
upper_sum ((f,A),g) is Relation-like NAT -defined REAL -valued V6() non empty total V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
lim (upper_sum ((f,A),g)) is V22() real ext-real Element of REAL
lower_sum ((f,A),g) is Relation-like NAT -defined REAL -valued V6() non empty total V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
lim (lower_sum ((f,A),g)) is V22() real ext-real Element of REAL
(lim (upper_sum ((f,A),g))) - (lim (lower_sum ((f,A),g))) is V22() real ext-real Element of REAL
(upper_sum ((f,A),g)) - (lower_sum ((f,A),g)) is Relation-like NAT -defined REAL -valued V6() non empty total V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
- (lower_sum ((f,A),g)) is Relation-like NAT -defined V6() total V35() V36() V37() set
- 1 is V22() real ext-real non positive set
(- 1) (#) (lower_sum ((f,A),g)) is Relation-like NAT -defined V6() total V35() V36() V37() set
(upper_sum ((f,A),g)) + (- (lower_sum ((f,A),g))) is Relation-like NAT -defined V6() total V35() V36() V37() set
X is V22() real ext-real Element of REAL
A /\ (dom f) is V45() V46() V47() Element of bool REAL
a1 is V22() real ext-real set
b1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
((upper_sum ((f,A),g)) - (lower_sum ((f,A),g))) . b1 is V22() real ext-real Element of REAL
(((upper_sum ((f,A),g)) - (lower_sum ((f,A),g))) . b1) - 0 is V22() real ext-real Element of REAL
abs ((((upper_sum ((f,A),g)) - (lower_sum ((f,A),g))) . b1) - 0) is V22() real ext-real Element of REAL
g . b1 is Relation-like NAT -defined REAL -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like Division of A
(upper_sum ((f,A),g)) . b1 is V22() real ext-real Element of REAL
- (lower_sum ((f,A),g)) is Relation-like NAT -defined REAL -valued V6() non empty total V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
(- (lower_sum ((f,A),g))) . b1 is V22() real ext-real Element of REAL
((upper_sum ((f,A),g)) . b1) + ((- (lower_sum ((f,A),g))) . b1) is V22() real ext-real Element of REAL
(lower_sum ((f,A),g)) . b1 is V22() real ext-real Element of REAL
- ((lower_sum ((f,A),g)) . b1) is V22() real ext-real Element of REAL
((upper_sum ((f,A),g)) . b1) + (- ((lower_sum ((f,A),g)) . b1)) is V22() real ext-real Element of REAL
x is Relation-like NAT -defined REAL -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like Division of A
upper_sum ((f,A),x) is V22() real ext-real Element of REAL
(upper_sum ((f,A),x)) + (- ((lower_sum ((f,A),g)) . b1)) is V22() real ext-real Element of REAL
lower_sum ((f,A),x) is V22() real ext-real Element of REAL
- (lower_sum ((f,A),x)) is V22() real ext-real Element of REAL
(upper_sum ((f,A),x)) + (- (lower_sum ((f,A),x))) is V22() real ext-real Element of REAL
(upper_sum ((f,A),x)) - (lower_sum ((f,A),x)) is V22() real ext-real Element of REAL
delta x is V22() real ext-real Element of REAL
(delta x) * ((f . (upper_bound A)) - (f . (lower_bound A))) is V22() real ext-real Element of REAL
a1 / ((f . (upper_bound A)) - (f . (lower_bound A))) is V22() real ext-real Element of REAL
b1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
x is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
(delta g) . x is V22() real ext-real Element of REAL
((delta g) . x) - 0 is V22() real ext-real Element of REAL
abs (((delta g) . x) - 0) is V22() real ext-real Element of REAL
abs ((delta g) . x) is V22() real ext-real Element of REAL
x is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
((upper_sum ((f,A),g)) - (lower_sum ((f,A),g))) . x is V22() real ext-real Element of REAL
(((upper_sum ((f,A),g)) - (lower_sum ((f,A),g))) . x) - 0 is V22() real ext-real Element of REAL
abs ((((upper_sum ((f,A),g)) - (lower_sum ((f,A),g))) . x) - 0) is V22() real ext-real Element of REAL
g . x is Relation-like NAT -defined REAL -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like Division of A
x is Relation-like NAT -defined REAL -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like Division of A
upper_sum ((f,A),x) is V22() real ext-real Element of REAL
lower_sum ((f,A),x) is V22() real ext-real Element of REAL
(upper_sum ((f,A),x)) - (lower_sum ((f,A),x)) is V22() real ext-real Element of REAL
abs ((upper_sum ((f,A),x)) - (lower_sum ((f,A),x))) is V22() real ext-real Element of REAL
(upper_sum ((f,A),g)) . x is V22() real ext-real Element of REAL
((upper_sum ((f,A),g)) . x) - (lower_sum ((f,A),x)) is V22() real ext-real Element of REAL
(((upper_sum ((f,A),g)) . x) - (lower_sum ((f,A),x))) - 0 is V22() real ext-real Element of REAL
abs ((((upper_sum ((f,A),g)) . x) - (lower_sum ((f,A),x))) - 0) is V22() real ext-real Element of REAL
(lower_sum ((f,A),g)) . x is V22() real ext-real Element of REAL
((upper_sum ((f,A),g)) . x) - ((lower_sum ((f,A),g)) . x) is V22() real ext-real Element of REAL
(((upper_sum ((f,A),g)) . x) - ((lower_sum ((f,A),g)) . x)) - 0 is V22() real ext-real Element of REAL
abs ((((upper_sum ((f,A),g)) . x) - ((lower_sum ((f,A),g)) . x)) - 0) is V22() real ext-real Element of REAL
- ((lower_sum ((f,A),g)) . x) is V22() real ext-real Element of REAL
((upper_sum ((f,A),g)) . x) + (- ((lower_sum ((f,A),g)) . x)) is V22() real ext-real Element of REAL
(((upper_sum ((f,A),g)) . x) + (- ((lower_sum ((f,A),g)) . x))) - 0 is V22() real ext-real Element of REAL
abs ((((upper_sum ((f,A),g)) . x) + (- ((lower_sum ((f,A),g)) . x))) - 0) is V22() real ext-real Element of REAL
- (lower_sum ((f,A),g)) is Relation-like NAT -defined REAL -valued V6() non empty total V30( NAT , REAL ) V35() V36() V37() Element of bool [:NAT,REAL:]
(- (lower_sum ((f,A),g))) . x is V22() real ext-real Element of REAL
((upper_sum ((f,A),g)) . x) + ((- (lower_sum ((f,A),g))) . x) is V22() real ext-real Element of REAL
(((upper_sum ((f,A),g)) . x) + ((- (lower_sum ((f,A),g))) . x)) - 0 is V22() real ext-real Element of REAL
abs ((((upper_sum ((f,A),g)) . x) + ((- (lower_sum ((f,A),g))) . x)) - 0) is V22() real ext-real Element of REAL
(delta g) . x is V22() real ext-real Element of REAL
((delta g) . x) * ((f . (upper_bound A)) - (f . (lower_bound A))) is V22() real ext-real Element of REAL
delta x is V22() real ext-real Element of REAL
(delta x) * ((f . (upper_bound A)) - (f . (lower_bound A))) is V22() real ext-real Element of REAL
b1 is ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded Element of NAT
lim ((upper_sum ((f,A),g)) - (lower_sum ((f,A),g))) is V22() real ext-real Element of REAL
A is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
dom f is V45() V46() V47() Element of bool REAL
- 1 is V22() real ext-real non positive Element of REAL
(- 1) (#) f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
((- 1) (#) f) | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
- f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
- 1 is V22() real ext-real non positive set
(- 1) (#) f is Relation-like REAL -defined V6() V35() V36() V37() set
((- f),A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
[:A,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:A,REAL:] is non empty non trivial V60() set
((- f),A) | A is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
g is V22() real ext-real Element of REAL
dom ((- f),A) is V45() V46() V47() Element of bool A
bool A is set
dom (- f) is V45() V46() V47() Element of bool REAL
(dom (- f)) /\ A is V45() V46() V47() Element of bool REAL
(dom f) /\ A is V45() V46() V47() Element of bool REAL
lower_bound A is V22() real ext-real Element of REAL
upper_bound A is V22() real ext-real Element of REAL
A /\ (dom ((- f),A)) is V45() V46() V47() Element of bool A
((- f),A) . (lower_bound A) is V22() real ext-real Element of REAL
X is set
((- f),A) . X is V22() real ext-real Element of REAL
a1 is V22() real ext-real Element of A
(- f) . a1 is V22() real ext-real Element of REAL
(- f) | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
((- f) | A) . a1 is V22() real ext-real Element of REAL
(- f) . (lower_bound A) is V22() real ext-real Element of REAL
((- f) | A) . (lower_bound A) is V22() real ext-real Element of REAL
A /\ (dom f) is V45() V46() V47() Element of bool REAL
A /\ (dom (- f)) is V45() V46() V47() Element of bool REAL
((- f),A) . (upper_bound A) is V22() real ext-real Element of REAL
X is set
((- f),A) . X is V22() real ext-real Element of REAL
a1 is V22() real ext-real Element of A
(- f) . a1 is V22() real ext-real Element of REAL
(- f) | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
((- f) | A) . a1 is V22() real ext-real Element of REAL
(- f) . (upper_bound A) is V22() real ext-real Element of REAL
((- f) | A) . (upper_bound A) is V22() real ext-real Element of REAL
A /\ (dom f) is V45() V46() V47() Element of bool REAL
A /\ (dom (- f)) is V45() V46() V47() Element of bool REAL
dom (- f) is V45() V46() V47() Element of bool REAL
(- 1) (#) ((- f),A) is Relation-like REAL -defined A -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
dom ((- f),A) is V45() V46() V47() Element of bool A
bool A is set
(dom (- f)) /\ A is V45() V46() V47() Element of bool REAL
(dom f) /\ A is V45() V46() V47() Element of bool REAL
dom ((- 1) (#) ((- f),A)) is V45() V46() V47() Element of bool A
(f,A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
dom (f,A) is V45() V46() V47() Element of bool A
g is V22() real ext-real Element of A
((- 1) (#) ((- f),A)) . g is V22() real ext-real Element of REAL
(f,A) . g is V22() real ext-real Element of REAL
((- f),A) . g is V22() real ext-real Element of REAL
(- f) . g is V22() real ext-real Element of REAL
f . g is V22() real ext-real Element of REAL
- (f . g) is V22() real ext-real Element of REAL
(- 1) * (- (f . g)) is V22() real ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
dom A is V45() V46() V47() Element of bool REAL
f is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
A | f is Relation-like REAL -defined f -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
g is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
A | g is Relation-like REAL -defined g -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
A is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
lower_bound f is V22() real ext-real Element of REAL
g is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
lower_bound g is V22() real ext-real Element of REAL
upper_bound g is V22() real ext-real Element of REAL
X is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
lower_bound X is V22() real ext-real Element of REAL
upper_bound X is V22() real ext-real Element of REAL
upper_bound f is V22() real ext-real Element of REAL
a1 is set
A `| a1 is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(A `| a1) | f is Relation-like REAL -defined f -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(f,(A `| a1)) is V22() real ext-real Element of REAL
((A `| a1),f) is Relation-like f -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:f,REAL:]
[:f,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:f,REAL:] is non empty non trivial V60() set
integral ((A `| a1),f) is V22() real ext-real Element of REAL
(g,(A `| a1)) is V22() real ext-real Element of REAL
((A `| a1),g) is Relation-like g -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:g,REAL:]
[:g,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:g,REAL:] is non empty non trivial V60() set
integral ((A `| a1),g) is V22() real ext-real Element of REAL
(X,(A `| a1)) is V22() real ext-real Element of REAL
((A `| a1),X) is Relation-like X -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:X,REAL:]
[:X,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:X,REAL:] is non empty non trivial V60() set
integral ((A `| a1),X) is V22() real ext-real Element of REAL
(g,(A `| a1)) + (X,(A `| a1)) is V22() real ext-real Element of REAL
b1 is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
x is set
x is V22() real ext-real Element of REAL
dom (A `| a1) is V45() V46() V47() Element of bool REAL
(A `| a1) | g is Relation-like REAL -defined g -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
x is set
x is V22() real ext-real Element of REAL
(A `| a1) | X is Relation-like REAL -defined X -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
A . (upper_bound X) is V22() real ext-real Element of REAL
A . (lower_bound X) is V22() real ext-real Element of REAL
(A . (upper_bound X)) - (A . (lower_bound X)) is V22() real ext-real Element of REAL
A . (upper_bound g) is V22() real ext-real Element of REAL
A . (lower_bound g) is V22() real ext-real Element of REAL
(A . (upper_bound g)) - (A . (lower_bound g)) is V22() real ext-real Element of REAL
A . (upper_bound f) is V22() real ext-real Element of REAL
A . (lower_bound f) is V22() real ext-real Element of REAL
(A . (upper_bound f)) - (A . (lower_bound f)) is V22() real ext-real Element of REAL
A is V22() real ext-real set
f is V22() real ext-real set
[.A,f.] is V45() V46() V47() closed interval Element of bool REAL
A is V22() real ext-real set
f is V22() real ext-real set
(A,f) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
g is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
((A,f),g) is V22() real ext-real Element of REAL
(g,(A,f)) is Relation-like (A,f) -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:(A,f),REAL:]
[:(A,f),REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:(A,f),REAL:] is non empty non trivial V60() set
integral (g,(A,f)) is V22() real ext-real Element of REAL
(f,A) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
((f,A),g) is V22() real ext-real Element of REAL
(g,(f,A)) is Relation-like (f,A) -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:(f,A),REAL:]
[:(f,A),REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:(f,A),REAL:] is non empty non trivial V60() set
integral (g,(f,A)) is V22() real ext-real Element of REAL
- ((f,A),g) is V22() real ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
(f,A) is V22() real ext-real Element of REAL
(A,f) is Relation-like f -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:f,REAL:]
[:f,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:f,REAL:] is non empty non trivial V60() set
integral (A,f) is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
X is V22() real ext-real Element of REAL
[.g,X.] is V45() V46() V47() closed interval Element of bool REAL
(g,X,A) is V22() real ext-real Element of REAL
a1 is V22() real ext-real Element of REAL
b1 is V22() real ext-real Element of REAL
[.a1,b1.] is V45() V46() V47() closed interval Element of bool REAL
(g,X) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
((g,X),A) is V22() real ext-real Element of REAL
(A,(g,X)) is Relation-like (g,X) -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:(g,X),REAL:]
[:(g,X),REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:(g,X),REAL:] is non empty non trivial V60() set
integral (A,(g,X)) is V22() real ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
(f,A) is V22() real ext-real Element of REAL
(A,f) is Relation-like f -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:f,REAL:]
[:f,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:f,REAL:] is non empty non trivial V60() set
integral (A,f) is V22() real ext-real Element of REAL
- (f,A) is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
X is V22() real ext-real Element of REAL
[.X,g.] is V45() V46() V47() closed interval Element of bool REAL
(g,X,A) is V22() real ext-real Element of REAL
a1 is V22() real ext-real Element of REAL
b1 is V22() real ext-real Element of REAL
[.a1,b1.] is V45() V46() V47() closed interval Element of bool REAL
(X,g) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
((X,g),A) is V22() real ext-real Element of REAL
(A,(X,g)) is Relation-like (X,g) -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:(X,g),REAL:]
[:(X,g),REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:(X,g),REAL:] is non empty non trivial V60() set
integral (A,(X,g)) is V22() real ext-real Element of REAL
- ((X,g),A) is V22() real ext-real Element of REAL
lower_bound f is V22() real ext-real Element of REAL
upper_bound f is V22() real ext-real Element of REAL
[.(lower_bound f),(upper_bound f).] is V45() V46() V47() closed interval Element of bool REAL
vol f is V22() real ext-real Element of REAL
(upper_bound f) - (upper_bound f) is V22() real ext-real Element of REAL
(g,X) is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
((g,X),A) is V22() real ext-real Element of REAL
(A,(g,X)) is Relation-like (g,X) -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:(g,X),REAL:]
[:(g,X),REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:(g,X),REAL:] is non empty non trivial V60() set
integral (A,(g,X)) is V22() real ext-real Element of REAL
A is non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound A is V22() real ext-real Element of REAL
lower_bound A is V22() real ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
g is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f . (upper_bound A) is V22() real ext-real Element of REAL
g . (upper_bound A) is V22() real ext-real Element of REAL
(f . (upper_bound A)) * (g . (upper_bound A)) is V22() real ext-real Element of REAL
f . (lower_bound A) is V22() real ext-real Element of REAL
g . (lower_bound A) is V22() real ext-real Element of REAL
(f . (lower_bound A)) * (g . (lower_bound A)) is V22() real ext-real Element of REAL
((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A))) is V22() real ext-real Element of REAL
X is V45() V46() V47() open Element of bool REAL
f `| X is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(f `| X) | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
g `| X is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(g `| X) | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(f `| X) (#) g is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(A,((f `| X) (#) g)) is V22() real ext-real Element of REAL
(((f `| X) (#) g),A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
[:A,REAL:] is Relation-like non empty non trivial V35() V36() V37() V60() set
bool [:A,REAL:] is non empty non trivial V60() set
integral (((f `| X) (#) g),A) is V22() real ext-real Element of REAL
f (#) (g `| X) is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(A,(f (#) (g `| X))) is V22() real ext-real Element of REAL
((f (#) (g `| X)),A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
integral ((f (#) (g `| X)),A) is V22() real ext-real Element of REAL
(((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (A,(f (#) (g `| X))) is V22() real ext-real Element of REAL
f (#) g is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(f (#) g) `| X is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
((f `| X) (#) g) + (f (#) (g `| X)) is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
g | X is Relation-like REAL -defined X -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
g | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
dom g is V45() V46() V47() Element of bool REAL
(g,A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
dom (g `| X) is V45() V46() V47() Element of bool REAL
((g `| X),A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
A /\ A is V45() V46() V47() interval Element of bool REAL
((f `| X) (#) g) | (A /\ A) is Relation-like REAL -defined A /\ A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(((f `| X) (#) g),A) | A is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
f | X is Relation-like REAL -defined X -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
f | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
dom f is V45() V46() V47() Element of bool REAL
(f,A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
dom (f `| X) is V45() V46() V47() Element of bool REAL
((f `| X),A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
((g `| X),A) | A is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
((f `| X),A) | A is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
dom ((f `| X) (#) g) is V45() V46() V47() Element of bool REAL
(dom (f `| X)) /\ (dom g) is V45() V46() V47() Element of bool REAL
(f (#) (g `| X)) | (A /\ A) is Relation-like REAL -defined A /\ A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
((f (#) (g `| X)),A) | A is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
(((f `| X) (#) g) + (f (#) (g `| X))) | (A /\ A) is Relation-like REAL -defined A /\ A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
((f (#) g) `| X) | A is Relation-like REAL -defined A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:REAL,REAL:]
(f (#) g) . (upper_bound A) is V22() real ext-real Element of REAL
(f (#) g) . (lower_bound A) is V22() real ext-real Element of REAL
dom (f (#) (g `| X)) is V45() V46() V47() Element of bool REAL
(dom f) /\ (dom (g `| X)) is V45() V46() V47() Element of bool REAL
(g,A) | A is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
((f `| X),A) (#) (g,A) is Relation-like REAL -defined A -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
(f,A) | A is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
(f,A) (#) ((g `| X),A) is Relation-like REAL -defined A -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
(((f `| X) (#) g),A) + ((f (#) (g `| X)),A) is Relation-like REAL -defined A -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
integral ((((f `| X) (#) g),A) + ((f (#) (g `| X)),A)) is V22() real ext-real Element of REAL
(integral (((f `| X) (#) g),A)) + (integral ((f (#) (g `| X)),A)) is V22() real ext-real Element of REAL
((((f `| X) (#) g) + (f (#) (g `| X))),A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
integral ((((f `| X) (#) g) + (f (#) (g `| X))),A) is V22() real ext-real Element of REAL
(A,((f `| X) (#) g)) + (A,(f (#) (g `| X))) is V22() real ext-real Element of REAL
(((f (#) g) `| X),A) is Relation-like A -defined REAL -defined REAL -valued V6() V35() V36() V37() Element of bool [:A,REAL:]
integral (((f (#) g) `| X),A) is V22() real ext-real Element of REAL
(A,((f (#) g) `| X)) is V22() real ext-real Element of REAL
((f (#) g) . (upper_bound A)) - ((f (#) g) . (lower_bound A)) is V22() real ext-real Element of REAL