:: INTEGRA2 semantic presentation

REAL is non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval set

NAT is non empty V12() epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() cardinal limit_cardinal left_end bounded_below Element of K19(REAL)

K19(REAL) is V12() V51() set

{} is set

RAT is non empty V12() complex-membered ext-real-membered real-membered rational-membered V50() V51() set

the Relation-like non-empty empty-yielding RAT -valued functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V34() V35() V36() V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() V52() V55() cardinal {} -element FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval set is Relation-like non-empty empty-yielding RAT -valued functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V34() V35() V36() V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() V52() V55() cardinal {} -element FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT

{{},1} is V51() set

COMPLEX is non empty V12() complex-membered V50() V51() set

omega is non empty V12() epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() cardinal limit_cardinal left_end bounded_below set

K19(omega) is V12() V51() set

K19(NAT) is V12() V51() set

INT is non empty V12() complex-membered ext-real-membered real-membered rational-membered integer-membered V50() V51() set

K20(COMPLEX,COMPLEX) is Relation-like V12() V34() V51() set

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

K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like V12() V34() V51() set

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

K20(REAL,REAL) is Relation-like V12() V34() V35() V36() V51() set

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

K20(K20(REAL,REAL),REAL) is Relation-like V12() V34() V35() V36() V51() set

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

K20(RAT,RAT) is Relation-like RAT -valued V12() V34() V35() V36() V51() set

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

K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued V12() V34() V35() V36() V51() set

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

K20(INT,INT) is Relation-like RAT -valued INT -valued V12() V34() V35() V36() V51() set

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

K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued V12() V34() V35() V36() V51() set

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

K20(NAT,NAT) is Relation-like RAT -valued INT -valued V12() V34() V35() V36() V37() V51() set

K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V12() V34() V35() V36() V37() V51() set

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

K291() is set

ExtREAL is non empty ext-real-membered interval set

K20(COMPLEX,REAL) is Relation-like V12() V34() V35() V36() V51() set

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

2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of NAT

0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

card {} is epsilon-transitive epsilon-connected ordinal cardinal set

+infty is non empty non real ext-real positive non negative set

-infty is non empty non real ext-real non positive negative set

A is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

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

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

e is V22() real ext-real set

[.(lower_bound A),(upper_bound A).] is complex-membered ext-real-membered real-membered interval Element of K19(REAL)

{ b

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

<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V34() V35() V36() V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() V52() V55() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered bounded_below bounded_above real-bounded interval FinSequence of REAL

A is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V34() V35() V36() V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() V52() V55() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered bounded_below bounded_above real-bounded interval FinSequence of REAL

e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

dom A is Relation-like non-empty empty-yielding RAT -valued functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V34() V35() V36() V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() V52() V55() cardinal {} -element FinSequence-like FinSequence-membered bounded_below bounded_above real-bounded interval Element of K19(NAT)

e + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

A . e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal Element of REAL

A . (e + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal Element of REAL

A is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like () FinSequence of REAL

dom A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)

e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

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

r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

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

b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b + (b + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

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

c

A . c

b + b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

X is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

X + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

1 + 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

len A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

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

c

b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b + (b + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

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

A . c

b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b + 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

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

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

b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal set

e + b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

e + b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

A is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

e is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() non-increasing V51() FinSequence-like FinSubsequence-like FinSequence of REAL

Rev e is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

dom (Rev e) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)

r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

r + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

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

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

len (Rev e) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

Seg (len (Rev e)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() len (Rev e) -element bounded_below bounded_above real-bounded Element of K19(NAT)

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

len e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

(len e) + 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

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

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

Seg (len e) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() len e -element bounded_below bounded_above real-bounded Element of K19(NAT)

b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal set

r + b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

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

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

dom e is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)

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

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

(len e) + r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

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

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

r is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like () FinSequence of REAL

b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

len b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

c

Rev c

X is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() non-increasing V51() FinSequence-like FinSubsequence-like FinSequence of REAL

X | b is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

i is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() non-increasing V51() FinSequence-like FinSubsequence-like FinSequence of REAL

Rev i is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

X . (b + 1) is V22() real ext-real Element of REAL

<*(X . (b + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V12() V34() V35() V36() V38() V39() V40() non-increasing V51() 1 -element FinSequence-like FinSubsequence-like FinSequence of REAL

(Rev i) ^ <*(X . (b + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

<*(X . (b + 1))*> ^ (Rev i) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

len X is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

len (X | b) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

(X | b) ^ <*(X . (b + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

Rev ((X | b) ^ <*(X . (b + 1))*>) is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

Rev X is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

b is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

len b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

c

Rev c

len A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

len b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() non-increasing V51() FinSequence-like FinSubsequence-like FinSequence of REAL

Rev b is Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

len b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

len (Rev b) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

rng (Rev b) is complex-membered ext-real-membered real-membered V51() bounded_below bounded_above real-bounded Element of K19(REAL)

rng b is complex-membered ext-real-membered real-membered V51() bounded_below bounded_above real-bounded Element of K19(REAL)

c

Coim (b,c

{c

b " {c

card (Coim (b,c

Coim ((Rev b),c

(Rev b) " {c

card (Coim ((Rev b),c

b " {c

card (b " {c

A is non empty set

e is Relation-like NAT -defined A -valued Function-like V51() FinSequence-like FinSubsequence-like FinSequence of A

len e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

mid (e,r,b) is Relation-like NAT -defined A -valued Function-like V51() FinSequence-like FinSubsequence-like FinSequence of A

b + 1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

mid (e,(b + 1),b) is Relation-like NAT -defined A -valued Function-like V51() FinSequence-like FinSubsequence-like FinSequence of A

(mid (e,r,b)) ^ (mid (e,(b + 1),b)) is Relation-like NAT -defined A -valued Function-like V51() FinSequence-like FinSubsequence-like FinSequence of A

mid (e,r,b) is Relation-like NAT -defined A -valued Function-like V51() FinSequence-like FinSubsequence-like FinSequence of A

len (mid (e,r,b)) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b -' r is V22() real ext-real non negative set

(b -' r) + 1 is non empty V22() real ext-real positive non negative Element of REAL

b - r is V22() real ext-real Element of REAL

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

len (mid (e,(b + 1),b)) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b -' (b + 1) is V22() real ext-real non negative set

(b -' (b + 1)) + 1 is non empty V22() real ext-real positive non negative Element of REAL

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

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

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

len ((mid (e,r,b)) ^ (mid (e,(b + 1),b))) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

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

b - r is V22() real ext-real Element of REAL

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

c

((mid (e,r,b)) ^ (mid (e,(b + 1),b))) . c

(mid (e,r,b)) . c

Seg (len ((mid (e,r,b)) ^ (mid (e,(b + 1),b)))) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() len ((mid (e,r,b)) ^ (mid (e,(b + 1),b))) -element bounded_below bounded_above real-bounded Element of K19(NAT)

dom ((mid (e,r,b)) ^ (mid (e,(b + 1),b))) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)

dom (mid (e,r,b)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)

Seg (len (mid (e,r,b))) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() len (mid (e,r,b)) -element bounded_below bounded_above real-bounded Element of K19(NAT)

(mid (e,r,b)) . c

c

(c

e . ((c

dom (mid (e,(b + 1),b)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)

X is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal set

(len (mid (e,r,b))) + X is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

X is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V51() cardinal set

(len (mid (e,r,b))) + X is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

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

b - (r - 1) is V22() real ext-real Element of REAL

(b - (r - 1)) + X is V22() real ext-real Element of REAL

((b - (r - 1)) + X) + r is V22() real ext-real Element of REAL

(((b - (r - 1)) + X) + r) - 1 is V22() real ext-real Element of REAL

e . ((((b - (r - 1)) + X) + r) - 1) is set

X + b is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

e . (X + b) is set

Seg (len (mid (e,(b + 1),b))) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() len (mid (e,(b + 1),b)) -element bounded_below bounded_above real-bounded Element of K19(NAT)

(mid (e,(b + 1),b)) . X is set

X + (b + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

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

e . ((X + (b + 1)) - 1) is set

(X + b) + 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

e . ((X + b) + 0) is set

dom (mid (e,r,b)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)

dom (mid (e,(b + 1),b)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded Element of K19(NAT)

len (mid (e,r,b)) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

b -' r is V22() real ext-real non negative set

(b -' r) + 1 is non empty V22() real ext-real positive non negative Element of REAL

A is complex-membered ext-real-membered real-membered set

e is V22() real ext-real set

e ** A is complex-membered ext-real-membered real-membered set

{e} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{e} ** A is complex-membered ext-real-membered real-membered set

{ K193(b

{e} ** A is ext-real-membered set

{ (b

e ** A is ext-real-membered set

A is non empty set

K20(A,REAL) is Relation-like V12() V34() V35() V36() V51() set

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

e is non empty set

r is Relation-like A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))

r | A is Relation-like A -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))

r | e is Relation-like A -defined e -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))

(r | e) | e is Relation-like A -defined e -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))

dom r is Element of K19(A)

K19(A) is set

A /\ (dom r) is Element of K19(A)

b is V22() real ext-real set

dom (r | e) is Element of K19(A)

e /\ (dom (r | e)) is Element of K19(A)

b is set

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

(dom r) /\ e is Element of K19(A)

(dom r) /\ A is Element of K19(A)

r . b is V22() real ext-real Element of REAL

A is non empty set

K20(A,REAL) is Relation-like V12() V34() V35() V36() V51() set

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

e is non empty set

r is Relation-like A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))

r | A is Relation-like A -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))

r | e is Relation-like A -defined e -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))

(r | e) | e is Relation-like A -defined e -defined A -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(A,REAL))

dom r is Element of K19(A)

K19(A) is set

A /\ (dom r) is Element of K19(A)

b is V22() real ext-real set

dom (r | e) is Element of K19(A)

e /\ (dom (r | e)) is Element of K19(A)

b is set

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

(dom r) /\ e is Element of K19(A)

(dom r) /\ A is Element of K19(A)

r . b is V22() real ext-real Element of REAL

A is complex-membered ext-real-membered real-membered set

e is V22() real ext-real set

(A,e) is complex-membered ext-real-membered real-membered Element of K19(REAL)

{e} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{e} ** A is complex-membered ext-real-membered real-membered set

{ K193(b

{e} ** A is ext-real-membered set

{ (b

e ** A is ext-real-membered set

r is complex-membered ext-real-membered real-membered set

b is V22() real ext-real set

(r,b) is complex-membered ext-real-membered real-membered Element of K19(REAL)

{b} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{b} ** r is complex-membered ext-real-membered real-membered set

{ K193(b

{b} ** r is ext-real-membered set

{ (b

b ** r is ext-real-membered set

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

e is complex-membered ext-real-membered real-membered Element of K19(REAL)

(e,A) is complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** e is complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** e is ext-real-membered set

{ (b

A ** e is ext-real-membered set

{ (A * b

r is set

b is ext-real Element of ExtREAL

A * b is ext-real set

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

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

r is set

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

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

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

e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** e is non empty complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** e is non empty ext-real-membered set

{ (b

A ** e is non empty ext-real-membered set

r is V22() real ext-real set

b is V22() real ext-real set

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

b is ext-real set

{ (A * b

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

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

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

e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** e is non empty complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** e is non empty ext-real-membered set

{ (b

A ** e is non empty ext-real-membered set

r is V22() real ext-real set

b is V22() real ext-real set

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

b is ext-real set

{ (A * b

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

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

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

e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** e is non empty complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** e is non empty ext-real-membered set

{ (b

A ** e is non empty ext-real-membered set

r is V22() real ext-real set

b is V22() real ext-real set

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

b is ext-real set

{ (A * b

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

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

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

e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** e is non empty complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** e is non empty ext-real-membered set

{ (b

A ** e is non empty ext-real-membered set

r is V22() real ext-real set

b is V22() real ext-real set

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

b is ext-real set

{ (A * b

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

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

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

e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** e is non empty complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** e is non empty ext-real-membered set

{ (b

A ** e is non empty ext-real-membered set

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

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

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

r is V22() real ext-real set

{ (A * b

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

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

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

b is V22() real ext-real set

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

{ (A * b

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

b is V22() real ext-real set

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

(b / A) * A is V22() real ext-real Element of REAL

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

e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** e is non empty complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** e is non empty ext-real-membered set

{ (b

A ** e is non empty ext-real-membered set

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

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

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

r is V22() real ext-real set

{ (A * b

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

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

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

b is V22() real ext-real set

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

{ (A * b

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

b is V22() real ext-real set

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

(b / A) * A is V22() real ext-real Element of REAL

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

e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** e is non empty complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** e is non empty ext-real-membered set

{ (b

A ** e is non empty ext-real-membered set

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

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

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

r is V22() real ext-real set

{ (A * b

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

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

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

b is V22() real ext-real set

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

{ (A * b

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

b is V22() real ext-real set

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

(b / A) * A is V22() real ext-real Element of REAL

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

e is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

(e,A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** e is non empty complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** e is non empty ext-real-membered set

{ (b

A ** e is non empty ext-real-membered set

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

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

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

r is V22() real ext-real set

{ (A * b

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

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

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

b is V22() real ext-real set

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

{ (A * b

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

b is V22() real ext-real set

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

(b / A) * A is V22() real ext-real Element of REAL

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

e is non empty set

K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set

K19(K20(e,REAL)) is V12() V51() set

r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))

A (#) r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))

rng (A (#) r) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

rng r is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

((rng r),A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** (rng r) is non empty complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** (rng r) is non empty ext-real-membered set

{ (b

A ** (rng r) is non empty ext-real-membered set

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

{ (A * b

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

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

dom r is non empty Element of K19(e)

K19(e) is set

c

r . c

dom (A (#) r) is non empty Element of K19(e)

(A (#) r) . c

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

dom (A (#) r) is non empty Element of K19(e)

K19(e) is set

b is Element of e

(A (#) r) . b is V22() real ext-real Element of REAL

dom r is non empty Element of K19(e)

r . b is V22() real ext-real Element of REAL

A * (r . b) is V22() real ext-real Element of REAL

{ (A * b

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

e is non empty set

K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set

K19(K20(e,REAL)) is V12() V51() set

r is non empty set

b is Relation-like e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))

b | r is Relation-like e -defined r -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))

A (#) (b | r) is Relation-like e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))

rng (A (#) (b | r)) is complex-membered ext-real-membered real-membered Element of K19(REAL)

rng (b | r) is complex-membered ext-real-membered real-membered Element of K19(REAL)

((rng (b | r)),A) is complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** (rng (b | r)) is complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** (rng (b | r)) is ext-real-membered set

{ (b

A ** (rng (b | r)) is ext-real-membered set

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

{ (A * b

c

A * c

dom (b | r) is Element of K19(e)

K19(e) is set

X is Element of e

(b | r) . X is V22() real ext-real Element of REAL

dom (A (#) (b | r)) is Element of K19(e)

(A (#) (b | r)) . X is V22() real ext-real Element of REAL

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

dom (A (#) (b | r)) is Element of K19(e)

K19(e) is set

c

(A (#) (b | r)) . c

dom (b | r) is Element of K19(e)

(b | r) . c

A * ((b | r) . c

{ (A * b

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

e is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set

K19(K20(e,REAL)) is V12() V51() set

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

r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))

r | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))

rng r is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

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

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

(A * (lower_bound (rng r))) * (vol e) is V22() real ext-real Element of REAL

A (#) r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))

upper_sum_set (A (#) r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))

divs e is non empty set

K20((divs e),REAL) is Relation-like V12() V34() V35() V36() V51() set

K19(K20((divs e),REAL)) is V12() V51() set

b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e

(upper_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL

(A (#) r) | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))

rng (A (#) r) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

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

(lower_bound (rng (A (#) r))) * (vol e) is V22() real ext-real Element of REAL

lower_sum ((A (#) r),b) is V22() real ext-real Element of REAL

upper_sum ((A (#) r),b) is V22() real ext-real Element of REAL

((rng r),A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** (rng r) is non empty complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** (rng r) is non empty ext-real-membered set

{ (b

A ** (rng r) is non empty ext-real-membered set

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

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

e is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set

K19(K20(e,REAL)) is V12() V51() set

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

r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))

r | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))

rng r is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

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

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

(A * (upper_bound (rng r))) * (vol e) is V22() real ext-real Element of REAL

A (#) r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))

upper_sum_set (A (#) r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))

divs e is non empty set

K20((divs e),REAL) is Relation-like V12() V34() V35() V36() V51() set

K19(K20((divs e),REAL)) is V12() V51() set

b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e

(upper_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL

(A (#) r) | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))

rng (A (#) r) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

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

(lower_bound (rng (A (#) r))) * (vol e) is V22() real ext-real Element of REAL

lower_sum ((A (#) r),b) is V22() real ext-real Element of REAL

upper_sum ((A (#) r),b) is V22() real ext-real Element of REAL

((rng r),A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** (rng r) is non empty complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** (rng r) is non empty ext-real-membered set

{ (b

A ** (rng r) is non empty ext-real-membered set

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

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

e is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set

K19(K20(e,REAL)) is V12() V51() set

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

r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))

r | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))

A (#) r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))

lower_sum_set (A (#) r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))

divs e is non empty set

K20((divs e),REAL) is Relation-like V12() V34() V35() V36() V51() set

K19(K20((divs e),REAL)) is V12() V51() set

rng r is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

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

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

(A * (upper_bound (rng r))) * (vol e) is V22() real ext-real Element of REAL

b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e

(lower_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL

(A (#) r) | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))

upper_sum ((A (#) r),b) is V22() real ext-real Element of REAL

rng (A (#) r) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

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

(upper_bound (rng (A (#) r))) * (vol e) is V22() real ext-real Element of REAL

lower_sum ((A (#) r),b) is V22() real ext-real Element of REAL

((rng r),A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** (rng r) is non empty complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** (rng r) is non empty ext-real-membered set

{ (b

A ** (rng r) is non empty ext-real-membered set

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

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

e is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

K20(e,REAL) is Relation-like V12() V34() V35() V36() V51() set

K19(K20(e,REAL)) is V12() V51() set

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

r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))

r | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))

A (#) r is Relation-like e -defined REAL -valued Function-like non empty total V30(e, REAL ) V34() V35() V36() Element of K19(K20(e,REAL))

lower_sum_set (A (#) r) is Relation-like divs e -defined REAL -valued Function-like non empty total V30( divs e, REAL ) V34() V35() V36() Element of K19(K20((divs e),REAL))

divs e is non empty set

K20((divs e),REAL) is Relation-like V12() V34() V35() V36() V51() set

K19(K20((divs e),REAL)) is V12() V51() set

rng r is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

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

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

(A * (lower_bound (rng r))) * (vol e) is V22() real ext-real Element of REAL

b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of e

(lower_sum_set (A (#) r)) . b is V22() real ext-real Element of REAL

(A (#) r) | e is Relation-like e -defined e -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(e,REAL))

upper_sum ((A (#) r),b) is V22() real ext-real Element of REAL

rng (A (#) r) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

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

(upper_bound (rng (A (#) r))) * (vol e) is V22() real ext-real Element of REAL

lower_sum ((A (#) r),b) is V22() real ext-real Element of REAL

((rng r),A) is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** (rng r) is non empty complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** (rng r) is non empty ext-real-membered set

{ (b

A ** (rng r) is non empty ext-real-membered set

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

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

e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

r is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

K20(r,REAL) is Relation-like V12() V34() V35() V36() V51() set

K19(K20(r,REAL)) is V12() V51() set

b is Relation-like r -defined REAL -valued Function-like non empty total V30(r, REAL ) V34() V35() V36() Element of K19(K20(r,REAL))

b | r is Relation-like r -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))

A (#) b is Relation-like r -defined REAL -valued Function-like non empty total V30(r, REAL ) V34() V35() V36() Element of K19(K20(r,REAL))

b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of r

dom b is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

upper_volume ((A (#) b),b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

(upper_volume ((A (#) b),b)) . e is V22() real ext-real Element of REAL

upper_volume (b,b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

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

A * ((upper_volume (b,b)) . e) is V22() real ext-real Element of REAL

divset (b,e) is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

b | (divset (b,e)) is Relation-like r -defined divset (b,e) -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))

dom (b | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(r)

K19(r) is set

dom b is non empty complex-membered ext-real-membered real-membered Element of K19(r)

(dom b) /\ (divset (b,e)) is complex-membered ext-real-membered real-membered Element of K19(REAL)

r /\ (divset (b,e)) is complex-membered ext-real-membered real-membered interval Element of K19(REAL)

rng (b | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(REAL)

rng b is non empty complex-membered ext-real-membered real-membered Element of K19(REAL)

(A (#) b) | (divset (b,e)) is Relation-like r -defined divset (b,e) -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))

rng ((A (#) b) | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(REAL)

upper_bound (rng ((A (#) b) | (divset (b,e)))) is V22() real ext-real Element of REAL

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

(upper_bound (rng ((A (#) b) | (divset (b,e))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL

A (#) (b | (divset (b,e))) is Relation-like r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))

rng (A (#) (b | (divset (b,e)))) is complex-membered ext-real-membered real-membered Element of K19(REAL)

upper_bound (rng (A (#) (b | (divset (b,e))))) is V22() real ext-real Element of REAL

(upper_bound (rng (A (#) (b | (divset (b,e)))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL

((rng (b | (divset (b,e)))),A) is complex-membered ext-real-membered real-membered Element of K19(REAL)

{A} is non empty V12() complex-membered ext-real-membered real-membered V51() 1 -element left_end right_end bounded_below bounded_above real-bounded set

{A} ** (rng (b | (divset (b,e)))) is complex-membered ext-real-membered real-membered set

{ K193(b

{A} ** (rng (b | (divset (b,e)))) is ext-real-membered set

{ (b

A ** (rng (b | (divset (b,e)))) is ext-real-membered set

upper_bound ((rng (b | (divset (b,e)))),A) is V22() real ext-real Element of REAL

(upper_bound ((rng (b | (divset (b,e)))),A)) * (vol (divset (b,e))) is V22() real ext-real Element of REAL

upper_bound (rng (b | (divset (b,e)))) is V22() real ext-real Element of REAL

A * (upper_bound (rng (b | (divset (b,e))))) is V22() real ext-real Element of REAL

(A * (upper_bound (rng (b | (divset (b,e)))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL

(upper_bound (rng (b | (divset (b,e))))) * (vol (divset (b,e))) is V22() real ext-real Element of REAL

A * ((upper_bound (rng (b | (divset (b,e))))) * (vol (divset (b,e)))) is V22() real ext-real Element of REAL

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

e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() cardinal V62() V63() bounded_below bounded_above real-bounded Element of NAT

r is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

K20(r,REAL) is Relation-like V12() V34() V35() V36() V51() set

K19(K20(r,REAL)) is V12() V51() set

b is Relation-like r -defined REAL -valued Function-like non empty total V30(r, REAL ) V34() V35() V36() Element of K19(K20(r,REAL))

b | r is Relation-like r -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))

A (#) b is Relation-like r -defined REAL -valued Function-like non empty total V30(r, REAL ) V34() V35() V36() Element of K19(K20(r,REAL))

b is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like Division of r

dom b is non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)

lower_volume ((A (#) b),b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

(lower_volume ((A (#) b),b)) . e is V22() real ext-real Element of REAL

upper_volume (b,b) is Relation-like NAT -defined REAL -valued Function-like non empty V34() V35() V36() V51() FinSequence-like FinSubsequence-like FinSequence of REAL

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

A * ((upper_volume (b,b)) . e) is V22() real ext-real Element of REAL

divset (b,e) is non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)

b | (divset (b,e)) is Relation-like r -defined divset (b,e) -defined r -defined REAL -valued Function-like V34() V35() V36() Element of K19(K20(r,REAL))

dom (b | (divset (b,e))) is complex-membered ext-real-membered real-membered Element of K19(r)

K19(r) is set

dom b is non empty complex-membered ext-real-membered