for A being ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) )
for x being ( ( real ) ( V22() real ext-real ) number ) holds
( x : ( ( real ) ( V22() real ext-real ) number ) in A : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) iff ( lower_bound A : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) <= x : ( ( real ) ( V22() real ext-real ) number ) & x : ( ( real ) ( V22() real ext-real ) number ) <= upper_bound A : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) ) ;

let IT be ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ;

for p being ( ( non-decreasing ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like non-decreasing ) FinSequence of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) )
for i, j being ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) st i : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) in dom p : ( ( non-decreasing ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like non-decreasing ) FinSequence of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded ) Element of K19(NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( V12() V51() ) set ) ) & j : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) in dom p : ( ( non-decreasing ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like non-decreasing ) FinSequence of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_below bounded_above real-bounded ) Element of K19(NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( V12() V51() ) set ) ) & i : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) <= j : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) holds
p : ( ( non-decreasing ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like non-decreasing ) FinSequence of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) . i : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) <= p : ( ( non-decreasing ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like non-decreasing ) FinSequence of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) . j : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ;

for p being ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ex q being ( ( non-decreasing ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like non-decreasing ) FinSequence of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) st p : ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ,q : ( ( non-decreasing ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like non-decreasing ) FinSequence of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) are_fiberwise_equipotent ;

for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V51() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for k1, k2, k3 being ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) st 1 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) <= k1 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) & k3 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V51() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) & k1 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) <= k2 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) & k2 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) < k3 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) holds
(mid (f : ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V51() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ,k1 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) ,k2 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V51() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ^ (mid (f : ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V51() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ,(k2 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) + 1 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) ) : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) ,k3 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V51() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V51() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) = mid (f : ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V51() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ,k1 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) ,k3 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V51() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ;

let A be ( ( real-membered ) ( complex-membered ext-real-membered real-membered ) set ) ;
let x be ( ( real ) ( V22() real ext-real ) number ) ;
:: original: **
redefine func x ** A -> ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) ;

for X, Y being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) PartFunc of ,) | X : ( ( non empty ) ( non empty ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) is bounded_above & Y : ( ( non empty ) ( non empty ) set ) c= X : ( ( non empty ) ( non empty ) set ) holds
(f : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) PartFunc of ,) | Y : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) | Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) is bounded_above ;

for X, Y being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) PartFunc of ,) | X : ( ( non empty ) ( non empty ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) is bounded_below & Y : ( ( non empty ) ( non empty ) set ) c= X : ( ( non empty ) ( non empty ) set ) holds
(f : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) PartFunc of ,) | Y : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) | Y : ( ( non empty ) ( non empty ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) Element of K19(K20(b₁ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) is bounded_below ;

for X being ( ( real-membered ) ( complex-membered ext-real-membered real-membered ) set )
for a being ( ( real ) ( V22() real ext-real ) number ) holds
( X : ( ( real-membered ) ( complex-membered ext-real-membered real-membered ) set ) is empty iff a : ( ( real ) ( V22() real ext-real ) number ) ** X : ( ( real-membered ) ( complex-membered ext-real-membered real-membered ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) is empty ) ;

for r being ( ( ) ( V22() real ext-real ) Real)
for X being ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) holds r : ( ( ) ( V22() real ext-real ) Real) ** X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) = { (r : ( ( ) ( V22() real ext-real ) Real) * x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) where x is ( ( ) ( V22() real ext-real ) Real) : x : ( ( ) ( V22() real ext-real ) Real) in X : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) } ;

for r being ( ( ) ( V22() real ext-real ) Real)
for X being ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) st X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) is bounded_above & 0 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) <= r : ( ( ) ( V22() real ext-real ) Real) holds
r : ( ( ) ( V22() real ext-real ) Real) ** X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) is bounded_above ;

for r being ( ( ) ( V22() real ext-real ) Real)
for X being ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) st X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) is bounded_above & r : ( ( ) ( V22() real ext-real ) Real) <= 0 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) holds
r : ( ( ) ( V22() real ext-real ) Real) ** X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) is bounded_below ;

for r being ( ( ) ( V22() real ext-real ) Real)
for X being ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) st X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) is bounded_below & 0 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) <= r : ( ( ) ( V22() real ext-real ) Real) holds
r : ( ( ) ( V22() real ext-real ) Real) ** X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) is bounded_below ;

for r being ( ( ) ( V22() real ext-real ) Real)
for X being ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) st X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) is bounded_below & r : ( ( ) ( V22() real ext-real ) Real) <= 0 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) holds
r : ( ( ) ( V22() real ext-real ) Real) ** X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) is bounded_above ;

for r being ( ( ) ( V22() real ext-real ) Real)
for X being ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) st X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) is bounded_above & 0 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) <= r : ( ( ) ( V22() real ext-real ) Real) holds
upper_bound (r : ( ( ) ( V22() real ext-real ) Real) ** X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) = r : ( ( ) ( V22() real ext-real ) Real) * (upper_bound X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ;

for r being ( ( ) ( V22() real ext-real ) Real)
for X being ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) st X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) is bounded_above & r : ( ( ) ( V22() real ext-real ) Real) <= 0 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) holds
lower_bound (r : ( ( ) ( V22() real ext-real ) Real) ** X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) = r : ( ( ) ( V22() real ext-real ) Real) * (upper_bound X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ;

for r being ( ( ) ( V22() real ext-real ) Real)
for X being ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) st X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) is bounded_below & 0 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) <= r : ( ( ) ( V22() real ext-real ) Real) holds
lower_bound (r : ( ( ) ( V22() real ext-real ) Real) ** X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) = r : ( ( ) ( V22() real ext-real ) Real) * (lower_bound X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ;

for r being ( ( ) ( V22() real ext-real ) Real)
for X being ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) st X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) is bounded_below & r : ( ( ) ( V22() real ext-real ) Real) <= 0 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) holds
upper_bound (r : ( ( ) ( V22() real ext-real ) Real) ** X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) = r : ( ( ) ( V22() real ext-real ) Real) * (lower_bound X : ( ( non empty ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ;

for r being ( ( ) ( V22() real ext-real ) Real)
for X being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like V30(b₂ : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30(b₂ : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Function of X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) holds rng (r : ( ( ) ( V22() real ext-real ) Real) (#) f : ( ( Function-like V30(b₂ : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30(b₂ : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Function of b₂ : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30(b₂ : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Element of K19(K20(b₂ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) Element of K19(REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) = r : ( ( ) ( V22() real ext-real ) Real) ** (rng f : ( ( Function-like V30(b₂ : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30(b₂ : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Function of b₂ : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) Element of K19(REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) ;

for r being ( ( ) ( V22() real ext-real ) Real)
for X, Z being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) PartFunc of ,) holds rng (r : ( ( ) ( V22() real ext-real ) Real) (#) (f : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) PartFunc of ,) | Z : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined b₃ : ( ( non empty ) ( non empty ) set ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) Element of K19(K20(b₂ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) Element of K19(K20(b₂ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K19(REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) = r : ( ( ) ( V22() real ext-real ) Real) ** (rng (f : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) PartFunc of ,) | Z : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined b₃ : ( ( non empty ) ( non empty ) set ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) Element of K19(K20(b₂ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K19(REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Subset of ( ( ) ( V12() V51() ) set ) ) ;

for r being ( ( ) ( V22() real ext-real ) Real)
for A being ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) )
for f being ( ( Function-like V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Function of A : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) )
for D being ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like ) Division of A : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) ) st f : ( ( Function-like V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Function of b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) | A : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) -defined b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) Element of K19(K20(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) is bounded & r : ( ( ) ( V22() real ext-real ) Real) >= 0 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) holds
(upper_sum_set (r : ( ( ) ( V22() real ext-real ) Real) (#) f : ( ( Function-like V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Function of b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Element of K19(K20(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) : ( ( Function-like V30( divs b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like divs b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30( divs b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Element of K19(K20((divs b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) . D : ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like ) Division of b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) >= (r : ( ( ) ( V22() real ext-real ) Real) * (lower_bound (rng f : ( ( Function-like V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Function of b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) Element of K19(REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) * (vol A : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ;

for r being ( ( ) ( V22() real ext-real ) Real)
for A being ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) )
for f being ( ( Function-like V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Function of A : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) )
for D being ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like ) Division of A : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) ) st f : ( ( Function-like V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Function of b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) | A : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) -defined b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like V34() V35() V36() ) Element of K19(K20(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) is bounded & r : ( ( ) ( V22() real ext-real ) Real) <= 0 : ( ( ) ( 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 : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) holds
(upper_sum_set (r : ( ( ) ( V22() real ext-real ) Real) (#) f : ( ( Function-like V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Function of b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Element of K19(K20(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) : ( ( Function-like V30( divs b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like divs b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30( divs b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Element of K19(K20((divs b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like V12() V34() V35() V36() V51() ) set ) ) : ( ( ) ( V12() V51() ) set ) ) . D : ( ( ) ( Relation-like NAT : ( ( ) ( 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 : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like one-to-one non empty V34() V35() V36() V38() V40() V51() FinSequence-like FinSubsequence-like ) Division of b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) >= (r : ( ( ) ( V22() real ext-real ) Real) * (upper_bound (rng f : ( ( Function-like V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) ( Relation-like b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) -defined REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) -valued Function-like non empty total V30(b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) V34() V35() V36() ) Function of b₂ : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) , REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) Element of K19(REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) * (vol A : ( ( non empty closed_interval ) ( non empty complex-membered ext-real-membered real-membered V78() closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( V12() V51() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V12() complex-membered ext-real-membered real-membered V50() V51() non bounded_below non bounded_above interval ) set ) ) ;