:: INTEGRA3 semantic presentation

REAL is non empty V12() V37() V58() V59() V60() V64() non bounded_below non bounded_above interval set

NAT is non empty V12() epsilon-transitive epsilon-connected ordinal V37() cardinal limit_cardinal V58() V59() V60() V61() V62() V63() V64() left_end bounded_below Element of K19(REAL)

K19(REAL) is V12() V37() set

COMPLEX is non empty V12() V37() V58() V64() set

omega is non empty V12() epsilon-transitive epsilon-connected ordinal V37() cardinal limit_cardinal V58() V59() V60() V61() V62() V63() V64() left_end bounded_below set

K19(omega) is V12() V37() set

K19(NAT) is V12() V37() set

INT is non empty V12() V37() V58() V59() V60() V61() V62() V64() set

K164(NAT) is V36() set

{} is Relation-like non-empty empty-yielding RAT -valued functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V37() V38() V41() cardinal {} -element FinSequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V58() V59() V60() V61() V62() V63() V64() bounded_below bounded_above real-bounded interval set

RAT is non empty V12() V37() V58() V59() V60() V61() V64() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

{{},1} is non empty V37() V41() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded set

K20(REAL,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(REAL,REAL)) is V12() V37() set

K20(COMPLEX,COMPLEX) is Relation-like V12() V37() complex-valued set

K19(K20(COMPLEX,COMPLEX)) is V12() V37() set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like V12() V37() complex-valued set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V12() V37() set

K20(K20(REAL,REAL),REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(K20(REAL,REAL),REAL)) is V12() V37() set

K20(RAT,RAT) is Relation-like RAT -valued V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(RAT,RAT)) is V12() V37() set

K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(K20(RAT,RAT),RAT)) is V12() V37() set

K20(INT,INT) is Relation-like RAT -valued INT -valued V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(INT,INT)) is V12() V37() set

K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(K20(INT,INT),INT)) is V12() V37() set

K20(NAT,NAT) is Relation-like RAT -valued INT -valued V12() V37() complex-valued ext-real-valued real-valued natural-valued set

K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V12() V37() complex-valued ext-real-valued real-valued natural-valued set

K19(K20(K20(NAT,NAT),NAT)) is V12() V37() set

K333() is set

ExtREAL is non empty V59() interval set

K20(NAT,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(NAT,REAL)) is V12() V37() set

K20(COMPLEX,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(COMPLEX,REAL)) is V12() V37() set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

0 is Relation-like non-empty empty-yielding RAT -valued functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V37() V38() V41() cardinal {} -element FinSequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V58() V59() V60() V61() V62() V63() V64() V69() V70() bounded_below bounded_above real-bounded interval Element of NAT

Seg 1 is non empty V12() V37() 1 -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

{1} is non empty V12() V37() V41() 1 -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded set

Seg 2 is non empty V37() 2 -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

{1,2} is non empty V37() V41() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded set

A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

A -' A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

(A -' A) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

A - A is V22() real ext-real Element of REAL

A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

chi (A,A) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))

K20(A,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(A,REAL)) is V12() V37() set

f is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

upper_volume ((chi (A,A)),f) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

sup (rng (upper_volume ((chi (A,A)),f))) is V22() real ext-real set

A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

divs A is non empty set

K20(NAT,(divs A)) is Relation-like V12() V37() set

K19(K20(NAT,(divs A))) is V12() V37() set

f is Relation-like Function-like non empty total V30( NAT , divs A) Element of K19(K20(NAT,(divs A)))

T is Relation-like Function-like non empty total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

e is Relation-like Function-like non empty total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

T . e is V22() real ext-real Element of REAL

e . e is V22() real ext-real Element of REAL

f . e is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

(A,(f . e)) is V22() real ext-real Element of REAL

chi (A,A) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))

K20(A,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(A,REAL)) is V12() V37() set

upper_volume ((chi (A,A)),(f . e)) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng (upper_volume ((chi (A,A)),(f . e))) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

sup (rng (upper_volume ((chi (A,A)),(f . e)))) is V22() real ext-real set

A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

f is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

(A,f) is V22() real ext-real Element of REAL

chi (A,A) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))

K20(A,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(A,REAL)) is V12() V37() set

upper_volume ((chi (A,A)),f) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

sup (rng (upper_volume ((chi (A,A)),f))) is V22() real ext-real set

T is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

(A,T) is V22() real ext-real Element of REAL

upper_volume ((chi (A,A)),T) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng (upper_volume ((chi (A,A)),T)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

sup (rng (upper_volume ((chi (A,A)),T))) is V22() real ext-real set

dom (upper_volume ((chi (A,A)),T)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

(upper_volume ((chi (A,A)),T)) . e is V22() real ext-real Element of REAL

len (upper_volume ((chi (A,A)),T)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

dom T is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

divset (T,e) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

vol (divset (T,e)) is V22() real ext-real Element of REAL

dom f is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

divset (f,e) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

vol (divset (f,e)) is V22() real ext-real Element of REAL

(upper_volume ((chi (A,A)),f)) . e is V22() real ext-real Element of REAL

len (upper_volume ((chi (A,A)),f)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

len f is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

dom (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

vol A is V22() real ext-real Element of REAL

f is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

dom f is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

len f is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

T is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

divset (f,T) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

vol (divset (f,T)) is V22() real ext-real Element of REAL

T is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

divset (f,T) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

upper_bound (divset (f,T)) is V22() real ext-real Element of REAL

lower_bound (divset (f,T)) is V22() real ext-real Element of REAL

vol (divset (f,T)) is V22() real ext-real Element of REAL

(upper_bound (divset (f,T))) - (lower_bound (divset (f,T))) is V22() real ext-real Element of REAL

(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

(len f) - 1 is V22() real ext-real Element of REAL

divset (f,(len f)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

upper_bound (divset (f,(len f))) is V22() real ext-real Element of REAL

f . (len f) is V22() real ext-real Element of REAL

lower_bound (divset (f,(len f))) is V22() real ext-real Element of REAL

f . ((len f) - 1) is V22() real ext-real Element of REAL

divset (f,(len f)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

upper_bound (divset (f,(len f))) is V22() real ext-real Element of REAL

f . (len f) is V22() real ext-real Element of REAL

upper_bound A is V22() real ext-real Element of REAL

lower_bound (divset (f,(len f))) is V22() real ext-real Element of REAL

lower_bound A is V22() real ext-real Element of REAL

(lower_bound A) + 0 is V22() real ext-real Element of REAL

(upper_bound A) - (lower_bound A) is V22() real ext-real Element of REAL

A is V22() real ext-real Element of REAL

f is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

T is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of f

dom T is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

lower_bound f is V22() real ext-real Element of REAL

upper_bound f is V22() real ext-real Element of REAL

rng T is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

T . e is V22() real ext-real Element of REAL

divset (T,e) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

lower_bound (divset (T,e)) is V22() real ext-real Element of REAL

upper_bound (divset (T,e)) is V22() real ext-real Element of REAL

e is V22() real ext-real Element of REAL

y is V22() real ext-real Element of REAL

lower_bound (divset (T,e)) is V22() real ext-real Element of REAL

upper_bound (divset (T,e)) is V22() real ext-real Element of REAL

e is V22() real ext-real Element of REAL

y is V22() real ext-real Element of REAL

len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

divset (T,(len T)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

upper_bound (divset (T,(len T))) is V22() real ext-real Element of REAL

T . (len T) is V22() real ext-real Element of REAL

e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal set

divset (T,e) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

upper_bound (divset (T,e)) is V22() real ext-real Element of REAL

divset (T,1) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

lower_bound (divset (T,1)) is V22() real ext-real Element of REAL

e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal set

divset (T,e) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

lower_bound (divset (T,e)) is V22() real ext-real Element of REAL

e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal set

divset (T,e) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

lower_bound (divset (T,e)) is V22() real ext-real Element of REAL

T . e is V22() real ext-real Element of REAL

e - 1 is V22() real ext-real Element of REAL

T . (e - 1) is V22() real ext-real Element of REAL

e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

upper_bound (divset (T,e)) is V22() real ext-real Element of REAL

T . e is V22() real ext-real Element of REAL

e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

divset (T,(e + 1)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

lower_bound (divset (T,(e + 1))) is V22() real ext-real Element of REAL

(e + 1) - 1 is V22() real ext-real Element of REAL

T . ((e + 1) - 1) is V22() real ext-real Element of REAL

A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

f is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

rng f is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

T is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

rng T is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

(rng f) \/ (rng T) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

f ^ T is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng (f ^ T) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

card (rng (f ^ T)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of omega

e is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng e is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)

len e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

e is Relation-like NAT -defined REAL -valued Function-like one-to-one V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing FinSequence of REAL

y is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing FinSequence of REAL

rng y is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

len y is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

y . (len y) is V22() real ext-real Element of REAL

upper_bound A is V22() real ext-real Element of REAL

len f is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

dom f is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

f . (len f) is V22() real ext-real Element of REAL

dom y is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

D is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

y . D is V22() real ext-real Element of REAL

D is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

rng D is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

card (rng f) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of omega

len D is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

len f is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

card (rng T) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of omega

len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

chi (A,A) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))

K20(A,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(A,REAL)) is V12() V37() set

f is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

(A,f) is V22() real ext-real Element of REAL

upper_volume ((chi (A,A)),f) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

sup (rng (upper_volume ((chi (A,A)),f))) is V22() real ext-real set

dom f is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

T is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

upper_volume ((chi (A,A)),T) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng (upper_volume ((chi (A,A)),T)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

inf (rng (upper_volume ((chi (A,A)),T))) is V22() real ext-real set

rng T is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

e is V22() real ext-real Element of REAL

e is V22() real ext-real Element of REAL

y is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

divset (f,y) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

(rng T) /\ (divset (f,y)) is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)

dom T is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

D is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

T . D is V22() real ext-real Element of REAL

p is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

T . p is V22() real ext-real Element of REAL

(T . D) - (T . p) is V22() real ext-real Element of REAL

abs ((T . D) - (T . p)) is V22() real ext-real Element of REAL

D + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len T) is non empty V37() len T -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

T . (D + 1) is V22() real ext-real Element of REAL

(T . D) - (T . (D + 1)) is V22() real ext-real Element of REAL

- ((T . D) - (T . (D + 1))) is V22() real ext-real Element of REAL

- ((T . D) - (T . p)) is V22() real ext-real Element of REAL

len (upper_volume ((chi (A,A)),T)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len (upper_volume ((chi (A,A)),T))) is non empty V37() len (upper_volume ((chi (A,A)),T)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

dom (upper_volume ((chi (A,A)),T)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

(upper_volume ((chi (A,A)),T)) . (D + 1) is V22() real ext-real Element of REAL

divset (T,(D + 1)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

upper_bound (divset (T,(D + 1))) is V22() real ext-real Element of REAL

- (abs ((T . D) - (T . p))) is V22() real ext-real Element of REAL

lower_bound (divset (T,(D + 1))) is V22() real ext-real Element of REAL

(D + 1) - 1 is V22() real ext-real Element of REAL

T . ((D + 1) - 1) is V22() real ext-real Element of REAL

vol (divset (T,(D + 1))) is V22() real ext-real Element of REAL

(T . (D + 1)) - (T . D) is V22() real ext-real Element of REAL

p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len T) is non empty V37() len T -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

T . (p + 1) is V22() real ext-real Element of REAL

(T . (p + 1)) - (T . p) is V22() real ext-real Element of REAL

len (upper_volume ((chi (A,A)),T)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len (upper_volume ((chi (A,A)),T))) is non empty V37() len (upper_volume ((chi (A,A)),T)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

dom (upper_volume ((chi (A,A)),T)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

(upper_volume ((chi (A,A)),T)) . (p + 1) is V22() real ext-real Element of REAL

divset (T,(p + 1)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

upper_bound (divset (T,(p + 1))) is V22() real ext-real Element of REAL

lower_bound (divset (T,(p + 1))) is V22() real ext-real Element of REAL

(p + 1) - 1 is V22() real ext-real Element of REAL

T . ((p + 1) - 1) is V22() real ext-real Element of REAL

vol (divset (T,(p + 1))) is V22() real ext-real Element of REAL

len f is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len f) is non empty V37() len f -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

len (upper_volume ((chi (A,A)),f)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len (upper_volume ((chi (A,A)),f))) is non empty V37() len (upper_volume ((chi (A,A)),f)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

dom (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

(upper_volume ((chi (A,A)),f)) . y is V22() real ext-real Element of REAL

upper_bound (divset (f,y)) is V22() real ext-real Element of REAL

lower_bound (divset (f,y)) is V22() real ext-real Element of REAL

(T . p) - (lower_bound (divset (f,y))) is V22() real ext-real Element of REAL

(upper_bound (divset (f,y))) - (lower_bound (divset (f,y))) is V22() real ext-real Element of REAL

(T . p) - (T . D) is V22() real ext-real Element of REAL

vol (divset (f,y)) is V22() real ext-real Element of REAL

- ((T . D) - (T . p)) is V22() real ext-real Element of REAL

len f is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len f) is non empty V37() len f -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

len (upper_volume ((chi (A,A)),f)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len (upper_volume ((chi (A,A)),f))) is non empty V37() len (upper_volume ((chi (A,A)),f)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

dom (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

(upper_volume ((chi (A,A)),f)) . y is V22() real ext-real Element of REAL

upper_bound (divset (f,y)) is V22() real ext-real Element of REAL

lower_bound (divset (f,y)) is V22() real ext-real Element of REAL

(T . D) - (lower_bound (divset (f,y))) is V22() real ext-real Element of REAL

(upper_bound (divset (f,y))) - (lower_bound (divset (f,y))) is V22() real ext-real Element of REAL

vol (divset (f,y)) is V22() real ext-real Element of REAL

A is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng A is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)

f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng f is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)

len A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

len f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

T is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

e is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of T

dom e is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

e is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of T

indx (e,e,A) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

indx (e,e,f) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

dom e is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

e . A is V22() real ext-real Element of REAL

e . (indx (e,e,A)) is V22() real ext-real Element of REAL

e . f is V22() real ext-real Element of REAL

e . (indx (e,e,f)) is V22() real ext-real Element of REAL

A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

T is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

e is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of T

dom e is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

e is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of T

indx (e,e,f) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

indx (e,e,A) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

e . A is V22() real ext-real Element of REAL

e . (indx (e,e,A)) is V22() real ext-real Element of REAL

dom e is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

e . f is V22() real ext-real Element of REAL

e . (indx (e,e,f)) is V22() real ext-real Element of REAL

A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

f is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A

(A,f) is V22() real ext-real Element of REAL

chi (A,A) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))

K20(A,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(A,REAL)) is V12() V37() set

upper_volume ((chi (A,A)),f) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

sup (rng (upper_volume ((chi (A,A)),f))) is V22() real ext-real set

rng f is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

T is V22() real ext-real Element of REAL

dom f is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

f . e is V22() real ext-real Element of REAL

len f is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len f) is non empty V37() len f -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

len (upper_volume ((chi (A,A)),f)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len (upper_volume ((chi (A,A)),f))) is non empty V37() len (upper_volume ((chi (A,A)),f)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

dom (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

(upper_volume ((chi (A,A)),f)) . e is V22() real ext-real Element of REAL

divset (f,e) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

vol (divset (f,e)) is V22() real ext-real Element of REAL

A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

K20(A,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(A,REAL)) is V12() V37() set

f is Relation-like Function-like non empty total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))

f | A is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))

rng f is non empty V58() V59() V60() Element of K19(REAL)

lower_bound (rng f) is V22() real ext-real Element of REAL

upper_bound (rng f) is V22() real ext-real Element of REAL

A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

K20(A,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(A,REAL)) is V12() V37() set

f is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

T is Relation-like Function-like non empty total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))

T | A is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))

rng T is non empty V58() V59() V60() Element of K19(REAL)

lower_bound (rng T) is V22() real ext-real Element of REAL

T | f is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))

rng (T | f) is V58() V59() V60() Element of K19(REAL)

lower_bound (rng (T | f)) is V22() real ext-real Element of REAL

upper_bound (rng (T | f)) is V22() real ext-real Element of REAL

upper_bound (rng T) is V22() real ext-real Element of REAL

dom T is non empty set

dom (T | f) is set

e is V22() real ext-real Element of REAL

(T | f) . e is V22() real ext-real Element of REAL

A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

f is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

T is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of f

dom T is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

divset (T,A) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

vol (divset (T,A)) is V22() real ext-real Element of REAL

(f,T) is V22() real ext-real Element of REAL

chi (f,f) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))

K20(f,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(f,REAL)) is V12() V37() set

upper_volume ((chi (f,f)),T) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng (upper_volume ((chi (f,f)),T)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

sup (rng (upper_volume ((chi (f,f)),T))) is V22() real ext-real set

len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len T) is non empty V37() len T -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

len (upper_volume ((chi (f,f)),T)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len (upper_volume ((chi (f,f)),T))) is non empty V37() len (upper_volume ((chi (f,f)),T)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

dom (upper_volume ((chi (f,f)),T)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

(upper_volume ((chi (f,f)),T)) . A is V22() real ext-real Element of REAL

A is V22() real ext-real Element of REAL

{A} is non empty V12() V37() 1 -element V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

f is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

T is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of f

len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

(len T) - 1 is V22() real ext-real Element of REAL

divset (T,(len T)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

rng T is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

(rng T) \/ {A} is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

e is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of f

rng e is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

indx (e,T,e) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

e | (indx (e,T,e)) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng (e | (indx (e,T,e))) is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)

T | e is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng (T | e) is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)

dom T is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

dom e is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

len e is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

lower_bound (divset (T,(len T))) is V22() real ext-real Element of REAL

T . e is V22() real ext-real Element of REAL

y is set

dom (e | (indx (e,T,e))) is V37() V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

D is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

(e | (indx (e,T,e))) . D is V22() real ext-real Element of REAL

len (e | (indx (e,T,e))) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

Seg (len (e | (indx (e,T,e)))) is V37() len (e | (indx (e,T,e))) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

Seg (indx (e,T,e)) is V37() indx (e,T,e) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

len (T | e) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

e . D is V22() real ext-real Element of REAL

e . (indx (e,T,e)) is V22() real ext-real Element of REAL

p is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

T . p is V22() real ext-real Element of REAL

Seg (len T) is non empty V37() len T -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

Seg e is V37() e -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

(T | e) . p is V22() real ext-real Element of REAL

dom (T | e) is V37() V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

dom (T | e) is V37() V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

(T | e) . e is V22() real ext-real Element of REAL

Seg e is V37() e -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

y is set

dom (T | e) is V37() V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

D is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

(T | e) . D is V22() real ext-real Element of REAL

len (T | e) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

Seg (len (T | e)) is V37() len (T | e) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

Seg e is V37() e -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

T . D is V22() real ext-real Element of REAL

indx (e,T,D) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

e . (indx (e,T,D)) is V22() real ext-real Element of REAL

e . (indx (e,T,e)) is V22() real ext-real Element of REAL

p is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

e . p is V22() real ext-real Element of REAL

Seg (indx (e,T,e)) is V37() indx (e,T,e) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

len (e | (indx (e,T,e))) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

Seg (len (e | (indx (e,T,e)))) is V37() len (e | (indx (e,T,e))) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

dom (e | (indx (e,T,e))) is V37() V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

(e | (indx (e,T,e))) . p is V22() real ext-real Element of REAL

A is V22() real ext-real Element of REAL

{A} is non empty V12() V37() 1 -element V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

f is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

K20(f,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set

K19(K20(f,REAL)) is V12() V37() set

T is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of f

len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

divset (T,(len T)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

rng T is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

(rng T) \/ {A} is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

(f,T) is V22() real ext-real Element of REAL

chi (f,f) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))

upper_volume ((chi (f,f)),T) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

rng (upper_volume ((chi (f,f)),T)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

sup (rng (upper_volume ((chi (f,f)),T))) is V22() real ext-real set

e is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of f

rng e is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)

e is Relation-like Function-like non empty total V30(f, REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))

e | f is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))

lower_volume (e,e) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

Sum (lower_volume (e,e)) is V22() real ext-real Element of REAL

K263() is Relation-like Function-like total V30(K20(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(K20(REAL,REAL),REAL))

K190(REAL,(lower_volume (e,e)),K263()) is V22() real ext-real Element of REAL

lower_volume (e,T) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

Sum (lower_volume (e,T)) is V22() real ext-real Element of REAL

K190(REAL,(lower_volume (e,T)),K263()) is V22() real ext-real Element of REAL

(Sum (lower_volume (e,e))) - (Sum (lower_volume (e,T))) is V22() real ext-real Element of REAL

rng e is non empty V58() V59() V60() Element of K19(REAL)

upper_bound (rng e) is V22() real ext-real Element of REAL

lower_bound (rng e) is V22() real ext-real Element of REAL

(upper_bound (rng e)) - (lower_bound (rng e)) is V22() real ext-real Element of REAL

((upper_bound (rng e)) - (lower_bound (rng e))) * (f,T) is V22() real ext-real Element of REAL

dom T is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

indx (e,T,(len T)) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

dom e is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

(len T) - 1 is V22() real ext-real Element of REAL

D is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

mid (T,1,D) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

T | D is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

indx (e,T,D) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

mid (e,1,(indx (e,T,D))) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

e | (indx (e,T,D)) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

len e is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

len (e | (indx (e,T,D))) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

rng (e | (indx (e,T,D))) is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)

rng (T | D) is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)

p is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

indx (e,T,p) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

Seg (len e) is non empty V37() len e -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

Seg D is V37() D -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

Seg (indx (e,T,D)) is V37() indx (e,T,D) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

(e | (indx (e,T,D))) . (indx (e,T,p)) is V22() real ext-real Element of REAL

e . (indx (e,T,p)) is V22() real ext-real Element of REAL

T . p is V22() real ext-real Element of REAL

T . (indx (e,T,p)) is V22() real ext-real Element of REAL

Seg D is V37() D -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

T . p is V22() real ext-real Element of REAL

(T | D) . p is V22() real ext-real Element of REAL

e . (indx (e,T,p)) is V22() real ext-real Element of REAL

e . p is V22() real ext-real Element of REAL

Seg (indx (e,T,D)) is V37() indx (e,T,D) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

(lower_volume (e,T)) | D is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

len ((lower_volume (e,T)) | D) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

(lower_volume (e,e)) | (indx (e,T,D)) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL

Seg (len e) is non empty V37() len e -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

len (lower_volume (e,e)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

Seg (len (lower_volume (e,e))) is non empty V37() len (lower_volume (e,e)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

dom (lower_volume (e,e)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

p is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal set

((lower_volume (e,T)) | D) . p is V22() real ext-real Element of REAL

((lower_volume (e,e)) | (indx (e,T,D))) . p is V22() real ext-real Element of REAL

len (lower_volume (e,T)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

H is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

Seg (len T) is non empty V37() len T -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

indx (e,T,H) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

Seg D is V37() D -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

Seg (indx (e,T,D)) is V37() indx (e,T,D) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)

T . H is V22() real ext-real Element of REAL

e . (indx (e,T,H)) is V22() real ext-real Element of REAL

divset (T,H) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

lower_bound (divset (T,H)) is V22() real ext-real Element of REAL

divset (e,(indx (e,T,H))) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

lower_bound (divset (e,(indx (e,T,H)))) is V22() real ext-real Element of REAL

upper_bound (divset (T,H)) is V22() real ext-real Element of REAL

upper_bound (divset (e,(indx (e,T,H)))) is V22() real ext-real Element of REAL

lower_bound f is V22() real ext-real Element of REAL

H - 1 is V22() real ext-real Element of REAL

h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

H + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT

(indx (e,T,H)) - 1 is V22() real ext-real Element of REAL

e . ((indx (e,T,H)) - 1) is V22() real ext-real Element of REAL

T . (H - 1) is V22() real ext-real Element of REAL

e . (H - 1) is V22() real ext-real Element of REAL

indx (e,T,h) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT

e . (indx (e,T,h)) is V22() real ext-real Element of REAL

[.(lower_bound (divset (T,H))),(upper_bound (divset (T,H))).] is V58() V59() V60() interval Element of K19(REAL)

Seg (len (lower_volume (e,T))) is non empty V37() len (lower_volume (e,T)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

dom (lower_volume (e,T)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

((lower_volume (e,T)) | D) . H is V22() real ext-real Element of REAL

(lower_volume (e,T)) . H is V22() real ext-real Element of REAL

e | (divset (e,(indx (e,T,H)))) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))

rng (e | (divset (e,(indx (e,T,H))))) is V58() V59() V60() Element of K19(REAL)

lower_bound (rng (e | (divset (e,(indx (e,T,H)))))) is V22() real ext-real Element of REAL

vol (divset (e,(indx (e,T,H)))) is V22() real ext-real Element of REAL

(lower_bound (rng (e | (divset (e,(indx (e,T,H))))))) * (vol (divset (e,(indx (e,T,H))))) is V22() real ext-real Element of REAL

((lower_volume (e,e)) | (indx (e,T,D))) . H is V22() real ext-real Element of REAL

((lower_v