:: INTEGRA4 semantic presentation

REAL is non empty non trivial non finite V68() V69() V70() V74() non bounded_below non bounded_above interval set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V42() V43() V68() V69() V70() V71() V72() V73() V74() left_end bounded_below Element of bool REAL
bool REAL is non trivial non finite set
COMPLEX is non empty non trivial non finite V68() V74() set
RAT is non empty non trivial non finite V68() V69() V70() V71() V74() set
INT is non empty non trivial non finite V68() V69() V70() V71() V72() V74() set
is non trivial V16() non finite complex-valued set
bool is non trivial non finite set
is non trivial V16() non finite complex-valued set
bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set

bool is non trivial non finite set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V42() V43() V68() V69() V70() V71() V72() V73() V74() left_end bounded_below set
bool omega is non trivial non finite set
bool NAT is non trivial non finite set
K270(NAT) is V52() set

{{},1} is non empty finite V41() V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded set
ExtREAL is non empty V69() interval set

bool is non trivial non finite set

bool is non trivial non finite set

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

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

() - () is V11() real ext-real Element of REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non trivial non finite set
integral (chi (A,A)) is V11() real ext-real Element of REAL

divs A is non empty set
upper_sum_set (chi (A,A)) is non empty V16() V19( divs A) V20( REAL ) Function-like total V30( divs A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:(divs A),REAL:]
[:(divs A),REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:(divs A),REAL:] is non trivial non finite set
dom (upper_sum_set (chi (A,A))) is non empty Element of bool (divs A)
bool (divs A) is set
(divs A) /\ (dom (upper_sum_set (chi (A,A)))) is Element of bool (divs A)
(divs A) /\ (divs A) is set

(upper_sum_set (chi (A,A))) /. f is V11() real ext-real Element of REAL
(upper_sum_set (chi (A,A))) . f is V11() real ext-real Element of REAL
(upper_sum_set (chi (A,A))) . f is V11() real ext-real Element of REAL

upper_sum ((chi (A,A)),r) is V11() real ext-real Element of REAL

Sum (upper_volume ((chi (A,A)),r)) is V11() real ext-real Element of REAL

K271(REAL,(upper_volume ((chi (A,A)),r)),K175()) is V11() real ext-real Element of REAL
(upper_sum_set (chi (A,A))) | (divs A) is V16() V19( divs A) V19( divs A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:(divs A),REAL:]
rng ((upper_sum_set (chi (A,A))) | (divs A)) is V68() V69() V70() Element of bool REAL
f is V11() real ext-real Element of REAL

rng (upper_sum_set (chi (A,A))) is non empty V68() V69() V70() Element of bool REAL

lower_bound (rng (upper_sum_set (chi (A,A)))) is V11() real ext-real Element of REAL
upper_integral (chi (A,A)) is V11() real ext-real Element of REAL
lower_sum_set (chi (A,A)) is non empty V16() V19( divs A) V20( REAL ) Function-like total V30( divs A, REAL ) complex-valued ext-real-valued real-valued Element of bool [:(divs A),REAL:]
dom (lower_sum_set (chi (A,A))) is non empty Element of bool (divs A)
(divs A) /\ (dom (lower_sum_set (chi (A,A)))) is Element of bool (divs A)

(lower_sum_set (chi (A,A))) /. r is V11() real ext-real Element of REAL
(lower_sum_set (chi (A,A))) . r is V11() real ext-real Element of REAL
(lower_sum_set (chi (A,A))) . r is V11() real ext-real Element of REAL

lower_sum ((chi (A,A)),r) is V11() real ext-real Element of REAL

Sum (lower_volume ((chi (A,A)),r)) is V11() real ext-real Element of REAL

K271(REAL,(lower_volume ((chi (A,A)),r)),K175()) is V11() real ext-real Element of REAL
(lower_sum_set (chi (A,A))) | (divs A) is V16() V19( divs A) V19( divs A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:(divs A),REAL:]
rng ((lower_sum_set (chi (A,A))) | (divs A)) is V68() V69() V70() Element of bool REAL
r is V11() real ext-real Element of REAL

rng (lower_sum_set (chi (A,A))) is non empty V68() V69() V70() Element of bool REAL

upper_bound (rng (lower_sum_set (chi (A,A)))) is V11() real ext-real Element of REAL
lower_integral (chi (A,A)) is V11() real ext-real Element of REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non trivial non finite set

rng f is V68() V69() V70() Element of bool REAL
r is V11() real ext-real Element of REAL

dom f is V68() V69() V70() Element of bool A
bool A is set
r is set
x is V11() real ext-real Element of REAL
(chi (A,A)) . x is V11() real ext-real Element of REAL
f . x is V11() real ext-real Element of REAL
r * 1 is V11() real ext-real Element of REAL
r is set
x is V11() real ext-real Element of A
f . x is V11() real ext-real Element of REAL
(chi (A,A)) . x is V11() real ext-real Element of REAL
r * 1 is V11() real ext-real Element of REAL

dom r is V68() V69() V70() Element of bool A
bool A is set
dom (chi (A,A)) is V68() V69() V70() Element of bool A
dom f is V68() V69() V70() Element of bool A
x is V11() real ext-real Element of A
f /. x is V11() real ext-real Element of REAL
r /. x is V11() real ext-real Element of REAL
f . x is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
(chi (A,A)) . x is V11() real ext-real Element of REAL
r * ((chi (A,A)) . x) is V11() real ext-real Element of REAL
r * 1 is V11() real ext-real Element of REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non trivial non finite set

rng f is non empty V68() V69() V70() Element of bool REAL

r is V11() real ext-real Element of REAL

r * (vol A) is V11() real ext-real Element of REAL

integral (chi (A,A)) is V11() real ext-real Element of REAL

rng (chi (A,A)) is V68() V69() V70() Element of bool REAL
(chi (A,A)) | A is V16() V19(A) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non trivial non finite set
f is V11() real ext-real Element of REAL

rng r is non empty V68() V69() V70() Element of bool REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non trivial non finite set
divs A is non empty set

[:(divs A),REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:(divs A),REAL:] is non trivial non finite set
dom () is non empty Element of bool (divs A)
bool (divs A) is set
(divs A) /\ (dom ()) is Element of bool (divs A)
(divs A) /\ (divs A) is set

() /. r is V11() real ext-real Element of REAL
() . r is V11() real ext-real Element of REAL

Seg (len r) is finite V44( len r) V68() V69() V70() V71() V72() V73() bounded_below bounded_above real-bounded Element of bool NAT

divset (x,(len x)) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (x,(len x))) is V11() real ext-real Element of REAL
sup (divset (x,(len x))) is V11() real ext-real set
x . (len x) is V11() real ext-real Element of REAL

lower_bound (divset (x,(len x))) is V11() real ext-real Element of REAL
inf (divset (x,(len x))) is V11() real ext-real set
[.(lower_bound (divset (x,(len x)))),(upper_bound (divset (x,(len x)))).] is V68() V69() V70() interval Element of bool REAL

[.(),().] is V68() V69() V70() interval Element of bool REAL
(upper_volume (f,x)) . 1 is V11() real ext-real Element of REAL
f | (divset (x,1)) is V16() V19(A) V19( divset (x,1)) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
rng (f | (divset (x,1))) is V68() V69() V70() Element of bool REAL
upper_bound (rng (f | (divset (x,1)))) is V11() real ext-real Element of REAL
(upper_bound (rng (f | (divset (x,1))))) * (vol A) is V11() real ext-real Element of REAL

() . r is V11() real ext-real Element of REAL
upper_sum (f,x) is V11() real ext-real Element of REAL
Sum (upper_volume (f,x)) is V11() real ext-real Element of REAL

K271(REAL,(upper_volume (f,x)),K175()) is V11() real ext-real Element of REAL

rng (() | (divs A)) is V68() V69() V70() Element of bool REAL
r is V11() real ext-real Element of REAL

rng () is non empty V68() V69() V70() Element of bool REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non trivial non finite set
divs A is non empty set

[:(divs A),REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:(divs A),REAL:] is non trivial non finite set
dom () is non empty Element of bool (divs A)
bool (divs A) is set
(divs A) /\ (dom ()) is Element of bool (divs A)
(divs A) /\ (divs A) is set

() /. r is V11() real ext-real Element of REAL
() . r is V11() real ext-real Element of REAL

Seg (len x) is non empty finite V44( len x) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

divset (x,(len x)) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (x,(len x))) is V11() real ext-real Element of REAL
sup (divset (x,(len x))) is V11() real ext-real set
x . (len x) is V11() real ext-real Element of REAL

lower_bound (divset (x,(len x))) is V11() real ext-real Element of REAL
inf (divset (x,(len x))) is V11() real ext-real set
[.(lower_bound (divset (x,(len x)))),(upper_bound (divset (x,(len x)))).] is V68() V69() V70() interval Element of bool REAL

[.(),().] is V68() V69() V70() interval Element of bool REAL
(lower_volume (f,x)) . 1 is V11() real ext-real Element of REAL
f | (divset (x,1)) is V16() V19(A) V19( divset (x,1)) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
rng (f | (divset (x,1))) is V68() V69() V70() Element of bool REAL
lower_bound (rng (f | (divset (x,1)))) is V11() real ext-real Element of REAL
(lower_bound (rng (f | (divset (x,1))))) * (vol A) is V11() real ext-real Element of REAL

() . r is V11() real ext-real Element of REAL
lower_sum (f,x) is V11() real ext-real Element of REAL
Sum (lower_volume (f,x)) is V11() real ext-real Element of REAL

K271(REAL,(lower_volume (f,x)),K175()) is V11() real ext-real Element of REAL

rng (() | (divs A)) is V68() V69() V70() Element of bool REAL
r is V11() real ext-real Element of REAL

rng () is non empty V68() V69() V70() Element of bool REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non trivial non finite set
divs A is non empty set

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non trivial non finite set

rng f is non empty V68() V69() V70() Element of bool REAL
lower_bound (rng f) is V11() real ext-real Element of REAL
upper_bound (rng f) is V11() real ext-real Element of REAL

rng r is non empty V68() V69() V70() Element of bool REAL

rng r is non empty V68() V69() V70() Element of bool REAL

(lower_bound (rng f)) * (vol A) is V11() real ext-real Element of REAL
dom f is non empty V68() V69() V70() Element of bool A
bool A is set
x is V11() real ext-real Element of REAL
f . x is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
f . x is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
dom r is non empty V68() V69() V70() Element of bool A
x is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
f . x is V11() real ext-real Element of REAL
dom r is non empty V68() V69() V70() Element of bool A

(upper_bound (rng f)) * (vol A) is V11() real ext-real Element of REAL
() / (vol A) is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
x * (vol A) is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
f . x is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
x * (vol A) is V11() real ext-real Element of REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non trivial non finite set
divs A is non empty set
[:NAT,(divs A):] is non trivial V16() non finite set
bool [:NAT,(divs A):] is non trivial non finite set

r is non empty V16() V19( NAT ) V20( divs A) Function-like total V30( NAT , divs A) Element of bool [:NAT,(divs A):]

lim () is V11() real ext-real Element of REAL

lim (lower_sum (f,r)) is V11() real ext-real Element of REAL

() . r is V11() real ext-real Element of REAL

rng (upper_volume ((chi (A,A)),(r . r))) is non empty finite V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
delta (r . r) is V11() real ext-real Element of REAL

vol (divset (y,x)) is V11() real ext-real Element of REAL

Seg (len y) is non empty finite V44( len y) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

Seg (len (upper_volume ((chi (A,A)),y))) is non empty finite V44( len (upper_volume ((chi (A,A)),y))) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
dom (upper_volume ((chi (A,A)),y)) is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
(upper_volume ((chi (A,A)),y)) . x is V11() real ext-real Element of REAL
rng (upper_volume ((chi (A,A)),y)) is non empty finite V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

{ b1 where b1 is V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = len y } is set
Seg (len y) is non empty finite V44( len y) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
K215((Seg (len y)),0) is non empty V16() V19( Seg (len y)) V20( RAT ) V20( INT ) V20() Function-like total V30( Seg (len y),) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(Seg (len y)),:]

bool [:(Seg (len y)),:] is finite V41() set

(upper_volume ((chi (A,A)),y)) . x is V11() real ext-real Element of REAL
((len y) |-> 0) . x is V11() real ext-real Element of REAL
Seg (len (upper_volume ((chi (A,A)),y))) is non empty finite V44( len (upper_volume ((chi (A,A)),y))) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

vol (divset (y,x)) is V11() real ext-real Element of REAL

Sum (upper_volume ((chi (A,A)),y)) is V11() real ext-real Element of REAL

K271(REAL,(upper_volume ((chi (A,A)),y)),K175()) is V11() real ext-real Element of REAL

(lower_sum (f,r)) . r is V11() real ext-real Element of REAL

divset (y,(len y)) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (y,(len y))) is V11() real ext-real Element of REAL
sup (divset (y,(len y))) is V11() real ext-real set
y . (len y) is V11() real ext-real Element of REAL

Seg (len y) is non empty finite V44( len y) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

lower_bound (divset (y,(len y))) is V11() real ext-real Element of REAL
inf (divset (y,(len y))) is V11() real ext-real set
[.(lower_bound (divset (y,(len y)))),(upper_bound (divset (y,(len y)))).] is V68() V69() V70() interval Element of bool REAL

[.(),().] is V68() V69() V70() interval Element of bool REAL
(lower_volume (f,y)) . 1 is V11() real ext-real Element of REAL
f | (divset (y,1)) is V16() V19(A) V19( divset (y,1)) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
rng (f | (divset (y,1))) is V68() V69() V70() Element of bool REAL
lower_bound (rng (f | (divset (y,1)))) is V11() real ext-real Element of REAL
(lower_bound (rng (f | (divset (y,1))))) * (vol A) is V11() real ext-real Element of REAL

Sum (lower_volume (f,y)) is V11() real ext-real Element of REAL

K271(REAL,(lower_volume (f,y)),K175()) is V11() real ext-real Element of REAL
lower_sum (f,y) is V11() real ext-real Element of REAL
(lower_sum (f,r)) . 1 is V11() real ext-real Element of REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non trivial non finite set
divs A is non empty set
[:NAT,(divs A):] is non trivial V16() non finite set
bool [:NAT,(divs A):] is non trivial non finite set

r is non empty V16() V19( NAT ) V20( divs A) Function-like total V30( NAT , divs A) Element of bool [:NAT,(divs A):]

lim () is V11() real ext-real Element of REAL

lim (upper_sum (f,r)) is V11() real ext-real Element of REAL

() . r is V11() real ext-real Element of REAL

delta (r . r) is V11() real ext-real Element of REAL

rng (upper_volume ((chi (A,A)),(r . r))) is non empty finite V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
sup (rng (upper_volume ((chi (A,A)),(r . r)))) is V11() real ext-real set

vol (divset (x,y)) is V11() real ext-real Element of REAL

Seg (len x) is non empty finite V44( len x) V68() V69() V70() V71() V72() V73() 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 finite V44( len (upper_volume ((chi (A,A)),x))) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
dom (upper_volume ((chi (A,A)),x)) is non empty finite V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
(upper_volume ((chi (A,A)),x)) . y is V11() real ext-real Element of REAL
rng (upper_volume ((chi (A,A)),x)) is non empty finite V68() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL

{ b1 where b1 is V16() V19( NAT ) V20( REAL ) Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = len x } is set
Seg (len x) is non empty finite V44( len x) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
K215((Seg (len x)),0) is non empty V16() V19( Seg (len x)) V20( RAT ) V20( INT ) V20() Function-like total V30( Seg (len x),) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of bool [:(Seg (len x)),:]

bool [:(Seg (len x)),:] is finite V41() set

(upper_volume ((chi (A,A)),x)) . y is V11() real ext-real Element of REAL
((len x) |-> 0) . y is V11() real ext-real Element of REAL
Seg (len (upper_volume ((chi (A,A)),x))) is non empty finite V44( len (upper_volume ((chi (A,A)),x))) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

vol (divset (x,y)) is V11() real ext-real Element of REAL

Sum (upper_volume ((chi (A,A)),x)) is V11() real ext-real Element of REAL

K271(REAL,(upper_volume ((chi (A,A)),x)),K175()) is V11() real ext-real Element of REAL

(upper_sum (f,r)) . r is V11() real ext-real Element of REAL

divset (y,(len y)) is non empty V68() V69() V70() V79() closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
upper_bound (divset (y,(len y))) is V11() real ext-real Element of REAL
sup (divset (y,(len y))) is V11() real ext-real set
y . (len y) is V11() real ext-real Element of REAL

Seg (len y) is non empty finite V44( len y) V68() V69() V70() V71() V72() V73() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

lower_bound (divset (y,(len y))) is V11() real ext-real Element of REAL
inf (divset (y,(len y))) is V11() real ext-real set
[.(lower_bound (divset (y,(len y)))),(upper_bound (divset (y,(len y)))).] is V68() V69() V70() interval Element of bool REAL

[.(),().] is V68() V69() V70() interval Element of bool REAL
(upper_volume (f,y)) . 1 is V11() real ext-real Element of REAL
f | (divset (y,1)) is V16() V19(A) V19( divset (y,1)) V19(A) V20( REAL ) Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
rng (f | (divset (y,1))) is V68() V69() V70() Element of bool REAL
upper_bound (rng (f | (divset (y,1)))) is V11() real ext-real Element of REAL
(upper_bound (rng (f | (divset (y,1))))) * (vol A) is V11() real ext-real Element of REAL

Sum (upper_volume (f,y)) is V11() real ext-real Element of REAL

K271(REAL,(upper_volume (f,y)),K175()) is V11() real ext-real Element of REAL
upper_sum (f,y) is V11() real ext-real Element of REAL
(upper_sum (f,r)) . 1 is V11() real ext-real Element of REAL

[:A,REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non trivial non finite set

rng f is non empty V68() V69() V70() Element of bool REAL
lower_bound (rng f) is V11() real ext-real Element of REAL

(lower_bound (rng f)) * (vol A) is V11() real ext-real Element of REAL

divs A is non empty set
[:(divs A),REAL:] is non trivial V16() non finite complex-valued ext-real-valued real-valued set
bool [:(divs A),REAL:] is non trivial non finite set
rng () is non empty V68() V69() V70() Element of bool REAL
r is ext-real set
dom () is non empty Element of bool (divs A)
bool (divs A) is set

() . r is V11() real ext-real Element of REAL

upper_sum (f,x) is V11() real ext-real Element of REAL
lower_sum (f,x) is V11() real ext-real Element of REAL
upper_bound (rng f) is V11() real ext-real Element of REAL
(upper_bound (rng f)) * (vol A) is V11() real ext-real Element of REAL

rng () is non empty V68() V69() V70() Element of bool REAL
r is ext-real set
dom () is non empty Element of bool (divs A)
bool (divs A) is set

() . r is V11() real ext-real Element of REAL

lower_sum (f,x) is V11() real ext-real Element of REAL
upper_sum (f,x) is V11() real ext-real Element of REAL

(vol A) / f is V11() real ext-real Element of REAL

r . r is V11() real ext-real Element of REAL

r . x is V11() real ext-real Element of REAL
((vol A) / f) * x is V11() real ext-real Element of REAL
((vol A) / f) * r is V11() real ext-real Element of REAL
() + (((vol A) / f) * x) is V11() real ext-real Element of REAL
() + (((vol A) / f) * r) is V11() real ext-real Element of REAL

r . (len r) is V11() real ext-real Element of REAL
((vol A) / f) * f is V11() real ext-real Element of REAL
() + (((vol A) / f) * f) is V11() real ext-real Element of REAL
() + (vol A) is V11() real ext-real Element of REAL

x is set

() - () is V11() real ext-real Element of REAL
() + (() - ()) is V11() real ext-real Element of REAL

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

r . x is V11() real ext-real Element of REAL
((vol A) / f) * x is V11() real ext-real Element of REAL
() + (((vol A) / f) * x) is V11() real ext-real Element of REAL

() - () is V11() real ext-real Element of REAL

x . y is V11() real ext-real Element of REAL
((vol A) / f) * y is V11() real ext-real Element of REAL
() + (((vol A) / f) * y) is V11() real ext-real Element of REAL

divs A is non empty set
[:NAT,(divs A):] is non trivial V16() non finite set
bool [:NAT,(divs A):] is non trivial non finite set

(vol A) / (f + 1) is V11() real ext-real Element of REAL

f is non empty V16() V19( NAT ) V20( divs A) Function-like total V30( NAT , divs A) Element of bool [:NAT,(divs A):]
r is non empty V16() V19( NAT ) V20( divs A) Function-like total V30( NAT , divs A) Element of bool [:NAT,(