:: ASYMPT_0 semantic presentation

REAL is non empty V2() non finite V67() V68() V69() V73() V80() V81() V83() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V67() V68() V69() V70() V71() V72() V73() V78() V80() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V2() non finite V67() V73() set
omega is non empty epsilon-transitive epsilon-connected ordinal V67() V68() V69() V70() V71() V72() V73() V78() V80() set
K6(omega) is set
K6(NAT) is set
RAT is non empty V2() non finite V67() V68() V69() V70() V73() set
INT is non empty V2() non finite V67() V68() V69() V70() V71() V73() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() V78() V80() Element of NAT
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional integer finite V59() V67() V68() V69() V70() V71() V72() V73() V80() V81() V82() V83() set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional integer finite V59() V66() V67() V68() V69() V70() V71() V72() V73() V80() V81() V82() V83() Element of NAT
- 1 is V11() real ext-real non positive integer Element of REAL
K7(NAT,REAL) is V33() V34() V35() set
K6(K7(NAT,REAL)) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() V78() V80() Element of NAT
F₃() is non empty set
F₁() is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
F₂() is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
{ F₄(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : ( F₁() <= b₁ & b₁ <= F₂() ) } is set
K6(F₃()) is set
{ F₄(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : ( F₁() <= b₁ & b₁ <= F₂() & S₁[b₁] ) } is set
F₄(F₁()) is Element of F₃()
IT is set
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F₄(IT1) is Element of F₃()
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F₄(IT1) is Element of F₃()
IT is set
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F₄(IT1) is Element of F₃()
F₂() is non empty set
F₁() is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
{ F₃(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : b₁ <= F₁() } is set
K6(F₂()) is set
{ F₃(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : ( 0 <= b₁ & b₁ <= F₁() ) } is set
IT is set
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F₃(IT1) is Element of F₂()
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F₃(IT1) is Element of F₂()
F₂() is non empty set
F₁() is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
{ F₃(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : not F₁() <= b₁ } is set
K6(F₂()) is set
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() V78() V80() Element of NAT
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
{ F₃(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : b₁ <= IT } is set
x is set
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F₃(f) is Element of F₂()
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F₃(f) is Element of F₂()
IT + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() V78() V80() Element of NAT
NAT --> 1 is non empty T-Sequence-like V16() V19( NAT ) V20( NAT ) V20( RAT ) V20( INT ) Function-like V26( NAT ) quasi_total V33() V34() V35() V36() Element of K6(K7(NAT,NAT))
K7(NAT,NAT) is V20( RAT ) V20( INT ) V33() V34() V35() V36() set
K6(K7(NAT,NAT)) is set
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . G is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . G is V11() real ext-real Element of REAL
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() V78() V80() Element of NAT
F . (G + 1) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . G is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . IT is V11() real ext-real Element of REAL
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . IT is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (G,IT) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . x is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
F + G is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (IT1,IT) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F + G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(F + G) . f is V11() real ext-real Element of REAL
G . f is V11() real ext-real Element of REAL
F . f is V11() real ext-real Element of REAL
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional integer finite V59() V66() V67() V68() V69() V70() V71() V72() V73() V80() V81() V82() V83() Element of NAT
(F . f) + (G . f) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is non empty V11() real ext-real positive non negative Element of REAL
G (#) F is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G (#) F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(G (#) F) . IT1 is V11() real ext-real Element of REAL
F . IT1 is V11() real ext-real Element of REAL
G * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional integer finite V59() V67() V68() V69() V70() V71() V72() V73() V80() V81() V82() V83() Element of REAL
G * (F . IT1) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is V11() real ext-real non negative Element of REAL
G + F is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G + F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(G + F) . IT1 is V11() real ext-real Element of REAL
F . IT1 is V11() real ext-real Element of REAL
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional integer finite V59() V66() V67() V68() V69() V70() V71() V72() V73() V80() V81() V82() V83() Element of NAT
G + (F . IT1) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is non empty V11() real ext-real positive non negative Element of REAL
G + F is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(F,G) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(F,G) . IT1 is V11() real ext-real Element of REAL
F . IT1 is V11() real ext-real Element of REAL
G + (F . IT1) is V11() real ext-real Element of REAL
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional integer finite V59() V66() V67() V68() V69() V70() V71() V72() V73() V80() V81() V82() V83() Element of NAT
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
IT is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT . IT1 is V11() real ext-real Element of REAL
F . IT1 is V11() real ext-real Element of REAL
G . IT1 is V11() real ext-real Element of REAL
max ((F . IT1),(G . IT1)) is V11() real ext-real Element of REAL
IT is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
IT1 is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT . x is V11() real ext-real Element of REAL
F . x is V11() real ext-real Element of REAL
G . x is V11() real ext-real Element of REAL
max ((F . x),(G . x)) is V11() real ext-real Element of REAL
IT1 . x is V11() real ext-real Element of REAL
IT is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
IT1 is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
x is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT . f is V11() real ext-real Element of REAL
x . f is V11() real ext-real Element of REAL
IT1 . f is V11() real ext-real Element of REAL
max ((x . f),(IT1 . f)) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(F,G) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(F,G) . IT1 is V11() real ext-real Element of REAL
G . IT1 is V11() real ext-real Element of REAL
F . IT1 is V11() real ext-real Element of REAL
max ((F . IT1),(G . IT1)) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
(F,G) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(F,G) . IT1 is V11() real ext-real Element of REAL
G . IT1 is V11() real ext-real Element of REAL
F . IT1 is V11() real ext-real Element of REAL
max ((F . IT1),(G . IT1)) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
F /" G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
F (#) (G ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(F /" G) . IT is V11() real ext-real Element of REAL
F . IT is V11() real ext-real Element of REAL
G . IT is V11() real ext-real Element of REAL
(F . IT) / (G . IT) is V11() real ext-real Element of REAL
G " is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
(G ") . IT is V11() real ext-real Element of REAL
(F . IT) * ((G ") . IT) is V11() real ext-real Element of REAL
(G . IT) " is V11() real ext-real Element of REAL
(F . IT) * ((G . IT) ") is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . IT is V11() real ext-real Element of REAL
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . IT1 is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
F . x is V11() real ext-real Element of REAL
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() V78() V80() Element of NAT
F . (x + 1) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
F /" G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
F (#) (G ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
lim (F /" G) is V11() real ext-real Element of REAL
G /" F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
F " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
G (#) (F ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
lim (G /" F) is V11() real ext-real Element of REAL
(lim (F /" G)) " is V11() real ext-real Element of REAL
abs (lim (F /" G)) is V11() real ext-real Element of REAL
(abs (lim (F /" G))) / 2 is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(abs (lim (F /" G))) * (abs (lim (F /" G))) is V11() real ext-real Element of REAL
0 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional integer finite V59() V66() V67() V68() V69() V70() V71() V72() V73() V80() V81() V82() V83() Element of NAT
((abs (lim (F /" G))) * (abs (lim (F /" G)))) / 2 is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t + f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(t + f) + f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f9 is V11() real ext-real set
f9 * ((abs (lim (F /" G))) / 2) is V11() real ext-real Element of REAL
(f9 * ((abs (lim (F /" G))) / 2)) / ((abs (lim (F /" G))) / 2) is V11() real ext-real Element of REAL
((abs (lim (F /" G))) / 2) " is V11() real ext-real Element of REAL
(f9 * ((abs (lim (F /" G))) / 2)) * (((abs (lim (F /" G))) / 2) ") is V11() real ext-real Element of REAL
((abs (lim (F /" G))) / 2) * (((abs (lim (F /" G))) / 2) ") is V11() real ext-real Element of REAL
f9 * (((abs (lim (F /" G))) / 2) * (((abs (lim (F /" G))) / 2) ")) is V11() real ext-real Element of REAL
f9 * 1 is V11() real ext-real Element of REAL
f9 * (((abs (lim (F /" G))) * (abs (lim (F /" G)))) / 2) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
((t + f) + f) + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(F /" G) . N is V11() real ext-real Element of REAL
abs ((F /" G) . N) is V11() real ext-real Element of REAL
(abs ((F /" G) . N)) * (abs (lim (F /" G))) is V11() real ext-real Element of REAL
(f9 * (((abs (lim (F /" G))) * (abs (lim (F /" G)))) / 2)) / ((abs ((F /" G) . N)) * (abs (lim (F /" G)))) is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative Element of REAL
(2 ") * ((abs (lim (F /" G))) * (abs (lim (F /" G)))) is V11() real ext-real Element of REAL
f9 * ((2 ") * ((abs (lim (F /" G))) * (abs (lim (F /" G))))) is V11() real ext-real Element of REAL
((abs ((F /" G) . N)) * (abs (lim (F /" G)))) " is V11() real ext-real Element of REAL
(f9 * ((2 ") * ((abs (lim (F /" G))) * (abs (lim (F /" G)))))) * (((abs ((F /" G) . N)) * (abs (lim (F /" G)))) ") is V11() real ext-real Element of REAL
f9 * (2 ") is V11() real ext-real Element of REAL
(abs (lim (F /" G))) * (abs ((F /" G) . N)) is V11() real ext-real Element of REAL
((abs (lim (F /" G))) * (abs ((F /" G) . N))) " is V11() real ext-real Element of REAL
((abs (lim (F /" G))) * (abs (lim (F /" G)))) * (((abs (lim (F /" G))) * (abs ((F /" G) . N))) ") is V11() real ext-real Element of REAL
(f9 * (2 ")) * (((abs (lim (F /" G))) * (abs (lim (F /" G)))) * (((abs (lim (F /" G))) * (abs ((F /" G) . N))) ")) is V11() real ext-real Element of REAL
(abs (lim (F /" G))) " is V11() real ext-real Element of REAL
(abs ((F /" G) . N)) " is V11() real ext-real Element of REAL
((abs (lim (F /" G))) ") * ((abs ((F /" G) . N)) ") is V11() real ext-real Element of REAL
((abs (lim (F /" G))) * (abs (lim (F /" G)))) * (((abs (lim (F /" G))) ") * ((abs ((F /" G) . N)) ")) is V11() real ext-real Element of REAL
(f9 * (2 ")) * (((abs (lim (F /" G))) * (abs (lim (F /" G)))) * (((abs (lim (F /" G))) ") * ((abs ((F /" G) . N)) "))) is V11() real ext-real Element of REAL
(abs (lim (F /" G))) * ((abs (lim (F /" G))) ") is V11() real ext-real Element of REAL
(abs (lim (F /" G))) * ((abs (lim (F /" G))) * ((abs (lim (F /" G))) ")) is V11() real ext-real Element of REAL
((abs (lim (F /" G))) * ((abs (lim (F /" G))) * ((abs (lim (F /" G))) "))) * ((abs ((F /" G) . N)) ") is V11() real ext-real Element of REAL
(f9 * (2 ")) * (((abs (lim (F /" G))) * ((abs (lim (F /" G))) * ((abs (lim (F /" G))) "))) * ((abs ((F /" G) . N)) ")) is V11() real ext-real Element of REAL
(abs (lim (F /" G))) * 1 is V11() real ext-real Element of REAL
((abs (lim (F /" G))) * 1) * ((abs ((F /" G) . N)) ") is V11() real ext-real Element of REAL
(f9 * (2 ")) * (((abs (lim (F /" G))) * 1) * ((abs ((F /" G) . N)) ")) is V11() real ext-real Element of REAL
(f9 * ((abs (lim (F /" G))) / 2)) * ((abs ((F /" G) . N)) ") is V11() real ext-real Element of REAL
(f9 * ((abs (lim (F /" G))) / 2)) / (abs ((F /" G) . N)) is V11() real ext-real Element of REAL
G . N is V11() real ext-real Element of REAL
F . N is V11() real ext-real Element of REAL
(F . N) / (G . N) is V11() real ext-real Element of REAL
((F /" G) . N) * (lim (F /" G)) is V11() real ext-real Element of REAL
abs (((F /" G) . N) * (lim (F /" G))) is V11() real ext-real Element of REAL
((F /" G) . N) - (lim (F /" G)) is V11() real ext-real Element of REAL
abs (((F /" G) . N) - (lim (F /" G))) is V11() real ext-real Element of REAL
(abs (((F /" G) . N) - (lim (F /" G)))) / ((abs ((F /" G) . N)) * (abs (lim (F /" G)))) is V11() real ext-real Element of REAL
(G /" F) . N is V11() real ext-real Element of REAL
((G /" F) . N) - ((lim (F /" G)) ") is V11() real ext-real Element of REAL
abs (((G /" F) . N) - ((lim (F /" G)) ")) is V11() real ext-real Element of REAL
(G . N) / (F . N) is V11() real ext-real Element of REAL
((G . N) / (F . N)) - ((lim (F /" G)) ") is V11() real ext-real Element of REAL
abs (((G . N) / (F . N)) - ((lim (F /" G)) ")) is V11() real ext-real Element of REAL
((F . N) / (G . N)) " is V11() real ext-real Element of REAL
(((F . N) / (G . N)) ") - ((lim (F /" G)) ") is V11() real ext-real Element of REAL
abs ((((F . N) / (G . N)) ") - ((lim (F /" G)) ")) is V11() real ext-real Element of REAL
((F /" G) . N) " is V11() real ext-real Element of REAL
(((F /" G) . N) ") - ((lim (F /" G)) ") is V11() real ext-real Element of REAL
abs ((((F /" G) . N) ") - ((lim (F /" G)) ")) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
lim F is V11() real ext-real Element of REAL
- (lim F) is V11() real ext-real Element of REAL
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (IT,G) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . (max (IT,G)) is V11() real ext-real Element of REAL
(F . (max (IT,G))) - (lim F) is V11() real ext-real Element of REAL
abs ((F . (max (IT,G))) - (lim F)) is V11() real ext-real Element of REAL
((F . (max (IT,G))) - (lim F)) + (lim F) is V11() real ext-real Element of REAL
(- (lim F)) + (lim F) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
lim F is V11() real ext-real Element of REAL
lim G is V11() real ext-real Element of REAL
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . IT1 is V11() real ext-real Element of REAL
G . IT1 is V11() real ext-real Element of REAL
(F . IT1) - (F . IT1) is V11() real ext-real Element of REAL
(G . IT1) - (F . IT1) is V11() real ext-real Element of REAL
G - F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
- F is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
- 1 is V11() real ext-real non positive integer set
(- 1) (#) F is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
G + (- F) is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
(G - F) . IT1 is V11() real ext-real Element of REAL
- F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
(- F) . IT1 is V11() real ext-real Element of REAL
(G . IT1) + ((- F) . IT1) is V11() real ext-real Element of REAL
- (F . IT1) is V11() real ext-real Element of REAL
(G . IT1) + (- (F . IT1)) is V11() real ext-real Element of REAL
lim (G - F) is V11() real ext-real Element of REAL
(lim G) - (lim F) is V11() real ext-real Element of REAL
0 + (lim F) is V11() real ext-real Element of REAL
((lim G) - (lim F)) + (lim F) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
F /" G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
F (#) (G ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
G /" F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
F " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
G (#) (F ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
lim (G /" F) is V11() real ext-real Element of REAL
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is V11() real ext-real set
1 / IT1 is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,IT) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(F /" G) . t is V11() real ext-real Element of REAL
IT1 * ((F /" G) . t) is V11() real ext-real Element of REAL
(1 / IT1) * IT1 is V11() real ext-real Element of REAL
F . t is V11() real ext-real Element of REAL
G . t is V11() real ext-real Element of REAL
(F . t) / (G . t) is V11() real ext-real Element of REAL
IT1 * ((F . t) / (G . t)) is V11() real ext-real Element of REAL
(G . t) " is V11() real ext-real Element of REAL
(F . t) * ((G . t) ") is V11() real ext-real Element of REAL
IT1 * ((F . t) * ((G . t) ")) is V11() real ext-real Element of REAL
(F . t) " is V11() real ext-real Element of REAL
(G . t) * ((F . t) ") is V11() real ext-real Element of REAL
(G . t) * 0 is V11() real ext-real Element of REAL
F " is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
(F ") . t is V11() real ext-real Element of REAL
(G . t) * ((F ") . t) is V11() real ext-real Element of REAL
(G /" F) . t is V11() real ext-real Element of REAL
((G /" F) . t) - 0 is V11() real ext-real Element of REAL
IT1 * (F . t) is V11() real ext-real Element of REAL
(IT1 * (F . t)) * ((F . t) ") is V11() real ext-real Element of REAL
(F . t) * ((F . t) ") is V11() real ext-real Element of REAL
IT1 * ((F . t) * ((F . t) ")) is V11() real ext-real Element of REAL
G (#) (F ") is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
(G (#) (F ")) . t is V11() real ext-real Element of REAL
IT1 * 1 is V11() real ext-real Element of REAL
(IT1 * (F . t)) * ((G . t) ") is V11() real ext-real Element of REAL
((IT1 * (F . t)) * ((G . t) ")) * (G . t) is V11() real ext-real Element of REAL
1 * (G . t) is V11() real ext-real Element of REAL
((G . t) ") * (G . t) is V11() real ext-real Element of REAL
(IT1 * (F . t)) * (((G . t) ") * (G . t)) is V11() real ext-real Element of REAL
(IT1 * (F . t)) * 1 is V11() real ext-real Element of REAL
abs (((G /" F) . t) - 0) is V11() real ext-real Element of REAL
1 * (G . t) is V11() real ext-real Element of REAL
(IT1 * (F . t)) * ((G . t) ") is V11() real ext-real Element of REAL
((IT1 * (F . t)) * ((G . t) ")) * (G . t) is V11() real ext-real Element of REAL
((G . t) ") * (G . t) is V11() real ext-real Element of REAL
(IT1 * (F . t)) * (((G . t) ") * (G . t)) is V11() real ext-real Element of REAL
(IT1 * (F . t)) * 1 is V11() real ext-real Element of REAL
abs (((G /" F) . t) - 0) is V11() real ext-real Element of REAL
Funcs (NAT,REAL) is non empty functional FUNCTION_DOMAIN of NAT , REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is set
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . IT1 is V11() real ext-real Element of REAL
1 * (F . IT1) is V11() real ext-real Element of REAL
IT1 is non empty functional set
x is V16() Function-like Element of IT1
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F is set
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
IT1 . t is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () () Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
IT is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
IT1 is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G . f is V11() real ext-real Element of REAL
F . f is V11() real ext-real Element of REAL
f * (F . f) is V11() real ext-real Element of REAL
{ H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : not x <= b₁ } is set
f is non empty finite V67() V68() V69() V78() V79() V80() V81() V82() Element of K6(REAL)
sup f is V11() real ext-real set
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G . t is V11() real ext-real Element of REAL
F . t is V11() real ext-real Element of REAL
(sup f) * (F . t) is V11() real ext-real Element of REAL
(G . t) / (F . t) is V11() real ext-real Element of REAL
((G . t) / (F . t)) * (F . t) is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G . t is V11() real ext-real Element of REAL
F . t is V11() real ext-real Element of REAL
IT1 * (F . t) is V11() real ext-real Element of REAL
(sup f) * (F . t) is V11() real ext-real Element of REAL
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G . t is V11() real ext-real Element of REAL
F . t is V11() real ext-real Element of REAL
t * (F . t) is V11() real ext-real Element of REAL
IT1 * (F . t) is V11() real ext-real Element of REAL
IT is V11() real ext-real Element of REAL
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G . x is V11() real ext-real Element of REAL
F . x is V11() real ext-real Element of REAL
IT * (F . x) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (x,IT) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
{ H₂(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : ( IT <= b₁ & b₁ <= max (x,IT) ) } is set
f is non empty finite V67() V68() V69() V78() V79() V80() V81() V82() Element of K6(REAL)
inf f is V11() real ext-real set
{ H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : ( IT <= b₁ & b₁ <= max (x,IT) ) } is set
f9 is non empty finite V67() V68() V69() V78() V79() V80() V81() V82() Element of K6(REAL)
sup f9 is V11() real ext-real set
(sup f9) / (inf f) is V11() real ext-real Element of COMPLEX
max (((sup f9) / (inf f)),IT1) is V11() real ext-real set
e is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G . N is V11() real ext-real Element of REAL
F . N is V11() real ext-real Element of REAL
e * (F . N) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . n is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . n is V11() real ext-real Element of REAL
IT1 * (F . N) is V11() real ext-real Element of REAL
G . x is V11() real ext-real Element of REAL
((sup f9) / (inf f)) * (inf f) is V11() real ext-real set
((sup f9) / (inf f)) * (F . N) is V11() real ext-real Element of REAL
(G . N) / (F . N) is V11() real ext-real Element of REAL
((G . N) / (F . N)) * (F . N) is V11() real ext-real Element of REAL
IT1 * (F . N) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(F,G) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
((F,G)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * ((F,G) . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F,G) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
((F,G)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * ((F,G) . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is set
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . f is V11() real ext-real Element of REAL
G . f is V11() real ext-real Element of REAL
max ((F . f),(G . f)) is V11() real ext-real Element of REAL
(F,G) . f is V11() real ext-real Element of REAL
1 * ((F,G) . f) is V11() real ext-real Element of REAL
(1 * ((F,G) . f)) + (1 * ((F,G) . f)) is V11() real ext-real Element of REAL
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() V78() V80() Element of NAT
(1 + 1) * ((F,G) . f) is V11() real ext-real Element of REAL
(F,G) . f is V11() real ext-real Element of REAL
(F . f) + (G . f) is V11() real ext-real Element of REAL
2 * ((F,G) . f) is V11() real ext-real Element of REAL
x * ((F,G) . f) is V11() real ext-real Element of REAL
x * (2 * ((F,G) . f)) is V11() real ext-real Element of REAL
IT1 . f is V11() real ext-real Element of REAL
2 * x is V11() real ext-real Element of REAL
(2 * x) * ((F,G) . f) is V11() real ext-real Element of REAL
2 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional integer finite V59() V66() V67() V68() V69() V70() V71() V72() V73() V80() V81() V82() V83() Element of NAT
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,t) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,(max (f,t))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . f9 is V11() real ext-real Element of REAL
G . f9 is V11() real ext-real Element of REAL
max ((F . f9),(G . f9)) is V11() real ext-real Element of REAL
0 + (G . f9) is V11() real ext-real Element of REAL
(F . f9) + (G . f9) is V11() real ext-real Element of REAL
(F . f9) + 0 is V11() real ext-real Element of REAL
(F,G) . f9 is V11() real ext-real Element of REAL
(F,G) . f9 is V11() real ext-real Element of REAL
x * ((F,G) . f9) is V11() real ext-real Element of REAL
x * ((F,G) . f9) is V11() real ext-real Element of REAL
IT1 . f9 is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . IT is V11() real ext-real Element of REAL
1 * (F . IT) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
IT1 is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is set
t is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
t is V11() real ext-real Element of REAL
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is V11() real ext-real Element of REAL
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t * IT1 is V11() real ext-real Element of REAL
max (t,IT1) is V11() real ext-real Element of REAL
max ((t * IT1),(max (t,IT1))) is V11() real ext-real Element of REAL
g9 is V11() real ext-real Element of REAL
max (f9,x) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max ((max (f9,x)),f) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT . e is V11() real ext-real Element of REAL
G . e is V11() real ext-real Element of REAL
IT1 * (G . e) is V11() real ext-real Element of REAL
t * (IT . e) is V11() real ext-real Element of REAL
t * (IT1 * (G . e)) is V11() real ext-real Element of REAL
(t * IT1) * (G . e) is V11() real ext-real Element of REAL
g9 * (G . e) is V11() real ext-real Element of REAL
t . e is V11() real ext-real Element of REAL
F . e is V11() real ext-real Element of REAL
t * (F . e) is V11() real ext-real Element of REAL
g9 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(IT) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (IT . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
G is non empty V11() real ext-real positive non negative Element of REAL
(F,G) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
((F,G)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * ((F,G) . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is set
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . f is V11() real ext-real Element of REAL
x * 1 is V11() real ext-real Element of REAL
F . f is V11() real ext-real Element of REAL
(x * 1) * (F . f) is V11() real ext-real Element of REAL
G " is non empty V11() real ext-real positive non negative Element of REAL
(G ") * G is V11() real ext-real non negative Element of REAL
x * ((G ") * G) is V11() real ext-real Element of REAL
(x * ((G ") * G)) * (F . f) is V11() real ext-real Element of REAL
x * (G ") is V11() real ext-real Element of REAL
G * (F . f) is V11() real ext-real Element of REAL
(x * (G ")) * (G * (F . f)) is V11() real ext-real Element of REAL
(F,G) . f is V11() real ext-real Element of REAL
(x * (G ")) * ((F,G) . f) is V11() real ext-real Element of REAL
0 * (G ") is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional integer finite V59() V67() V68() V69() V70() V71() V72() V73() V80() V81() V82() V83() Element of REAL
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . f is V11() real ext-real Element of REAL
(F,G) . f is V11() real ext-real Element of REAL
x * ((F,G) . f) is V11() real ext-real Element of REAL
F . f is V11() real ext-real Element of REAL
G * (F . f) is V11() real ext-real Element of REAL
x * (G * (F . f)) is V11() real ext-real Element of REAL
x * G is V11() real ext-real Element of REAL
(x * G) * (F . f) is V11() real ext-real Element of REAL
0 * G is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional integer finite V59() V67() V68() V69() V70() V71() V72() V73() V80() V81() V82() V83() Element of REAL
F is V11() real ext-real non negative Element of REAL
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
IT is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(IT) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (IT . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(IT,F) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
((IT,F)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * ((IT,F) . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT . f is V11() real ext-real Element of REAL
(IT . f) + 0 is V11() real ext-real Element of REAL
(IT . f) + F is V11() real ext-real Element of REAL
(IT,F) . f is V11() real ext-real Element of REAL
x * (IT . f) is V11() real ext-real Element of REAL
x * ((IT,F) . f) is V11() real ext-real Element of REAL
IT1 . f is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
F /" G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
F (#) (G ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
lim (F /" G) is V11() real ext-real Element of REAL
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
2 * (lim (F /" G)) is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,t) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max ((max (f,t)),f) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G . g9 is V11() real ext-real Element of REAL
(F /" G) . g9 is V11() real ext-real Element of REAL
((F /" G) . g9) - (lim (F /" G)) is V11() real ext-real Element of REAL
abs (((F /" G) . g9) - (lim (F /" G))) is V11() real ext-real Element of REAL
1 * (lim (F /" G)) is V11() real ext-real Element of REAL
(1 * (lim (F /" G))) + (1 * (lim (F /" G))) is V11() real ext-real Element of REAL
F . g9 is V11() real ext-real Element of REAL
G " is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
(G ") . g9 is V11() real ext-real Element of REAL
(F . g9) * ((G ") . g9) is V11() real ext-real Element of REAL
(G . g9) " is V11() real ext-real Element of REAL
(F . g9) * ((G . g9) ") is V11() real ext-real Element of REAL
((F . g9) * ((G . g9) ")) * (G . g9) is V11() real ext-real Element of REAL
(2 * (lim (F /" G))) * (G . g9) is V11() real ext-real Element of REAL
((G . g9) ") * (G . g9) is V11() real ext-real Element of REAL
(F . g9) * (((G . g9) ") * (G . g9)) is V11() real ext-real Element of REAL
(F . g9) * 1 is V11() real ext-real Element of REAL
2 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional integer finite V59() V66() V67() V68() V69() V70() V71() V72() V73() V80() V81() V82() V83() Element of NAT
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
F /" G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
F (#) (G ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
lim (F /" G) is V11() real ext-real Element of REAL
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
G /" F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
F " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
G (#) (F ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
lim (G /" F) is V11() real ext-real Element of REAL
(lim (F /" G)) " is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
F /" G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
F (#) (G ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
lim (F /" G) is V11() real ext-real Element of REAL
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
1 / f is V11() real ext-real Element of REAL
NAT --> (1 / f) is non empty T-Sequence-like V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
max (t,x) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G . n is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
f * (F . n) is V11() real ext-real Element of REAL
(G . n) " is V11() real ext-real Element of REAL
(G . n) * ((G . n) ") is V11() real ext-real Element of REAL
(f * (F . n)) * ((G . n) ") is V11() real ext-real Element of REAL
f " is V11() real ext-real Element of REAL
(f ") * 1 is V11() real ext-real Element of REAL
(F . n) * ((G . n) ") is V11() real ext-real Element of REAL
f * ((F . n) * ((G . n) ")) is V11() real ext-real Element of REAL
(f ") * (f * ((F . n) * ((G . n) "))) is V11() real ext-real Element of REAL
(f ") * f is V11() real ext-real Element of REAL
((f ") * f) * ((F . n) * ((G . n) ")) is V11() real ext-real Element of REAL
1 * ((F . n) * ((G . n) ")) is V11() real ext-real Element of REAL
1 * (F . n) is V11() real ext-real Element of REAL
(1 * (F . n)) * ((G . n) ") is V11() real ext-real Element of REAL
(1 * (F . n)) / (G . n) is V11() real ext-real Element of REAL
(F /" G) . n is V11() real ext-real Element of REAL
t is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
t . n is V11() real ext-real Element of REAL
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
n is V11() real ext-real set
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t . N is V11() real ext-real Element of REAL
g9 is V11() real ext-real Element of REAL
(t . N) - g9 is V11() real ext-real Element of REAL
abs ((t . N) - g9) is V11() real ext-real Element of REAL
(1 / f) - (1 / f) is V11() real ext-real Element of REAL
abs ((1 / f) - (1 / f)) is V11() real ext-real Element of REAL
abs 0 is V11() real ext-real V66() Element of REAL
g9 is V11() real ext-real Element of REAL
g9 is V11() real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t . e is V11() real ext-real Element of REAL
(t . e) - (1 / f) is V11() real ext-real Element of REAL
abs ((t . e) - (1 / f)) is V11() real ext-real Element of REAL
lim t is V11() real ext-real Element of REAL
(1 / f) * f is V11() real ext-real Element of REAL
0 * f is V11() real ext-real Element of REAL
max (IT,IT1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max ((max (IT,IT1)),x) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(F /" G) . t is V11() real ext-real Element of REAL
((F /" G) . t) - 0 is V11() real ext-real Element of REAL
abs (((F /" G) . t) - 0) is V11() real ext-real Element of REAL
F . t is V11() real ext-real Element of REAL
G " is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
(G ") . t is V11() real ext-real Element of REAL
(F . t) * ((G ") . t) is V11() real ext-real Element of REAL
G . t is V11() real ext-real Element of REAL
(G . t) " is V11() real ext-real Element of REAL
(F . t) * ((G . t) ") is V11() real ext-real Element of REAL
((F . t) * ((G . t) ")) * (G . t) is V11() real ext-real Element of REAL
1 * (G . t) is V11() real ext-real Element of REAL
((G . t) ") * (G . t) is V11() real ext-real Element of REAL
(F . t) * (((G . t) ") * (G . t)) is V11() real ext-real Element of REAL
(F . t) * 1 is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
F /" G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
F (#) (G ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
G /" F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
F " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
G (#) (F ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
lim (G /" F) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is set
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . IT1 is V11() real ext-real Element of REAL
1 * (F . IT1) is V11() real ext-real Element of REAL
IT1 is non empty functional set
x is V16() Function-like Element of IT1
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F is set
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (G . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
IT1 . t is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (G . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,IT) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G . t is V11() real ext-real Element of REAL
x * (G . t) is V11() real ext-real Element of REAL
IT1 . t is V11() real ext-real Element of REAL
x " is V11() real ext-real Element of REAL
(x ") * (x * (G . t)) is V11() real ext-real Element of REAL
(x ") * (IT1 . t) is V11() real ext-real Element of REAL
(x ") * x is V11() real ext-real Element of REAL
((x ") * x) * (G . t) is V11() real ext-real Element of REAL
1 * (G . t) is V11() real ext-real Element of REAL
F . t is V11() real ext-real Element of REAL
(x ") * (F . t) is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
IT1 is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (x,f) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT . t is V11() real ext-real Element of REAL
F . t is V11() real ext-real Element of REAL
IT1 * (F . t) is V11() real ext-real Element of REAL
IT1 " is V11() real ext-real Element of REAL
(IT1 ") * (IT . t) is V11() real ext-real Element of REAL
(IT1 ") * (IT1 * (F . t)) is V11() real ext-real Element of REAL
(IT1 ") * IT1 is V11() real ext-real Element of REAL
((IT1 ") * IT1) * (F . t) is V11() real ext-real Element of REAL
1 * (F . t) is V11() real ext-real Element of REAL
G . t is V11() real ext-real Element of REAL
(IT1 ") * (G . t) is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (G . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(IT) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (IT . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
F /" G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
F (#) (G ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
lim (F /" G) is V11() real ext-real Element of REAL
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (G . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is set
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . t is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . t is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
F /" G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
F (#) (G ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
lim (F /" G) is V11() real ext-real Element of REAL
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (G . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
F /" G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
F (#) (G ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (G . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
G /" F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
F " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
G (#) (F ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
lim (G /" F) is V11() real ext-real Element of REAL
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () () Element of K6(K7(NAT,REAL))
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () () Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
IT1 is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . f is V11() real ext-real Element of REAL
f * (F . f) is V11() real ext-real Element of REAL
G . f is V11() real ext-real Element of REAL
{ H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : not x <= b₁ } is set
f is non empty finite V67() V68() V69() V78() V79() V80() V81() V82() Element of K6(REAL)
inf f is V11() real ext-real set
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . t is V11() real ext-real Element of REAL
(inf f) * (F . t) is V11() real ext-real Element of REAL
G . t is V11() real ext-real Element of REAL
(G . t) / (F . t) is V11() real ext-real Element of REAL
((G . t) / (F . t)) * (F . t) is V11() real ext-real Element of REAL
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G . t is V11() real ext-real Element of REAL
F . t is V11() real ext-real Element of REAL
(G . t) / (F . t) is V11() real ext-real Element of REAL
(F . t) " is V11() real ext-real Element of REAL
(G . t) * ((F . t) ") is V11() real ext-real Element of REAL
0 * ((F . t) ") is V11() real ext-real Element of REAL
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . f9 is V11() real ext-real Element of REAL
t * (F . f9) is V11() real ext-real Element of REAL
G . f9 is V11() real ext-real Element of REAL
IT1 * (F . f9) is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . t is V11() real ext-real Element of REAL
IT1 * (F . t) is V11() real ext-real Element of REAL
G . t is V11() real ext-real Element of REAL
(inf f) * (F . t) is V11() real ext-real Element of REAL
IT is V11() real ext-real Element of REAL
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . IT1 is V11() real ext-real Element of REAL
IT * (F . IT1) is V11() real ext-real Element of REAL
G . IT1 is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(F,G) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
((F,G)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * ((F,G) . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(F,G) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
((F,G)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * ((F,G) . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is set
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (IT,IT1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (t,(max (IT,IT1))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . f9 is V11() real ext-real Element of REAL
G . f9 is V11() real ext-real Element of REAL
(F,G) . f9 is V11() real ext-real Element of REAL
max ((F . f9),(G . f9)) is V11() real ext-real Element of REAL
(F,G) . f9 is V11() real ext-real Element of REAL
((F,G) . f9) + 0 is V11() real ext-real Element of REAL
(F . f9) + (G . f9) is V11() real ext-real Element of REAL
((F,G) . f9) + 0 is V11() real ext-real Element of REAL
(G . f9) + (F . f9) is V11() real ext-real Element of REAL
f * ((F,G) . f9) is V11() real ext-real Element of REAL
f * ((F,G) . f9) is V11() real ext-real Element of REAL
f . f9 is V11() real ext-real Element of REAL
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (t,(max (IT,IT1))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . f9 is V11() real ext-real Element of REAL
G . f9 is V11() real ext-real Element of REAL
max ((F . f9),(G . f9)) is V11() real ext-real Element of REAL
(F . f9) + (G . f9) is V11() real ext-real Element of REAL
1 * (max ((F . f9),(G . f9))) is V11() real ext-real Element of REAL
(1 * (max ((F . f9),(G . f9)))) + (1 * (max ((F . f9),(G . f9)))) is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative Element of REAL
(2 ") * ((F . f9) + (G . f9)) is V11() real ext-real Element of REAL
2 * (max ((F . f9),(G . f9))) is V11() real ext-real Element of REAL
(2 ") * (2 * (max ((F . f9),(G . f9)))) is V11() real ext-real Element of REAL
(F,G) . f9 is V11() real ext-real Element of REAL
(2 ") * ((F,G) . f9) is V11() real ext-real Element of REAL
f * ((2 ") * ((F,G) . f9)) is V11() real ext-real Element of REAL
f * (max ((F . f9),(G . f9))) is V11() real ext-real Element of REAL
(F,G) . f9 is V11() real ext-real Element of REAL
f * ((F,G) . f9) is V11() real ext-real Element of REAL
f . f9 is V11() real ext-real Element of REAL
f * (2 ") is V11() real ext-real Element of REAL
(f * (2 ")) * ((F,G) . f9) is V11() real ext-real Element of REAL
f * 0 is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) /\ (F) is set
G is Element of (F) /\ (F)
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) /\ (F) is set
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂, b₃ being V11() real ext-real Element of REAL ex b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & not b₃ <= 0 & ( for b₅ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₄ <= b₅ or ( b₃ * (F . b₅) <= b₁ . b₅ & b₁ . b₅ <= b₂ * (F . b₅) ) ) ) ) } is set
IT is set
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,t) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . n is V11() real ext-real Element of REAL
t * (F . n) is V11() real ext-real Element of REAL
IT1 . n is V11() real ext-real Element of REAL
f * (F . n) is V11() real ext-real Element of REAL
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,t) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . g9 is V11() real ext-real Element of REAL
f * (F . g9) is V11() real ext-real Element of REAL
IT1 . g9 is V11() real ext-real Element of REAL
f * 0 is V11() real ext-real Element of REAL
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . g9 is V11() real ext-real Element of REAL
F . g9 is V11() real ext-real Element of REAL
x * (F . g9) is V11() real ext-real Element of REAL
f * (F . g9) is V11() real ext-real Element of REAL
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) /\ (F) is set
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (G . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) /\ (G) is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) /\ (F) is set
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (G . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) /\ (G) is set
IT is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(IT) is non empty functional FUNCTION_DOMAIN of NAT , REAL
(IT) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (IT . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(IT) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (IT . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(IT) /\ (IT) is set
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () () Element of K6(K7(NAT,REAL))
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () () Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) /\ (F) is set
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂, b₃ being V11() real ext-real Element of REAL ex b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & not b₃ <= 0 & ( for b₅ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₄ <= b₅ or ( b₃ * (F . b₅) <= b₁ . b₅ & b₁ . b₅ <= b₂ * (F . b₅) ) ) ) ) } is set
IT is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
IT1 is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is V11() real ext-real Element of REAL
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . t is V11() real ext-real Element of REAL
t * (F . t) is V11() real ext-real Element of REAL
G . t is V11() real ext-real Element of REAL
f * (F . t) is V11() real ext-real Element of REAL
{ H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : not f <= b₁ } is set
f is non empty finite V67() V68() V69() V78() V79() V80() V81() V82() Element of K6(REAL)
sup f is V11() real ext-real set
inf f is V11() real ext-real set
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . f9 is V11() real ext-real Element of REAL
(inf f) * (F . f9) is V11() real ext-real Element of REAL
G . f9 is V11() real ext-real Element of REAL
(G . f9) / (F . f9) is V11() real ext-real Element of REAL
((G . f9) / (F . f9)) * (F . f9) is V11() real ext-real Element of REAL
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G . f9 is V11() real ext-real Element of REAL
F . f9 is V11() real ext-real Element of REAL
(sup f) * (F . f9) is V11() real ext-real Element of REAL
(G . f9) / (F . f9) is V11() real ext-real Element of REAL
((G . f9) / (F . f9)) * (F . f9) is V11() real ext-real Element of REAL
min ((inf f),x) is V11() real ext-real set
max ((sup f),IT1) is V11() real ext-real set
n is V11() real ext-real Element of REAL
e is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . N is V11() real ext-real Element of REAL
G . N is V11() real ext-real Element of REAL
(F . N) " is V11() real ext-real Element of REAL
(G . N) * ((F . N) ") is V11() real ext-real Element of REAL
0 * ((F . N) ") is V11() real ext-real Element of REAL
(G . N) / (F . N) is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G . N is V11() real ext-real Element of REAL
F . N is V11() real ext-real Element of REAL
(G . N) / (F . N) is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . N is V11() real ext-real Element of REAL
e * (F . N) is V11() real ext-real Element of REAL
G . N is V11() real ext-real Element of REAL
n * (F . N) is V11() real ext-real Element of REAL
(inf f) * (F . N) is V11() real ext-real Element of REAL
(sup f) * (F . N) is V11() real ext-real Element of REAL
x * (F . N) is V11() real ext-real Element of REAL
IT1 * (F . N) is V11() real ext-real Element of REAL
IT is V11() real ext-real Element of REAL
IT1 is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . x is V11() real ext-real Element of REAL
IT1 * (F . x) is V11() real ext-real Element of REAL
G . x is V11() real ext-real Element of REAL
IT * (F . x) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(F,G) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
((F,G)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
((F,G)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * ((F,G) . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
((F,G)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * ((F,G) . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
((F,G)) /\ ((F,G)) is set
(F,G) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
((F,G)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
((F,G)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * ((F,G) . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
((F,G)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * ((F,G) . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
((F,G)) /\ ((F,G)) is set
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂, b₃ being V11() real ext-real Element of REAL ex b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & not b₃ <= 0 & ( for b₅ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₄ <= b₅ or ( b₃ * ((F,G) . b₅) <= b₁ . b₅ & b₁ . b₅ <= b₂ * ((F,G) . b₅) ) ) ) ) } is set
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂, b₃ being V11() real ext-real Element of REAL ex b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & not b₃ <= 0 & ( for b₅ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₄ <= b₅ or ( b₃ * ((F,G) . b₅) <= b₁ . b₅ & b₁ . b₅ <= b₂ * ((F,G) . b₅) ) ) ) ) } is set
x is set
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V11() real ext-real Element of REAL
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is V11() real ext-real Element of REAL
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (IT1,IT) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (t,(max (IT1,IT))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G . g9 is V11() real ext-real Element of REAL
F . g9 is V11() real ext-real Element of REAL
max ((F . g9),(G . g9)) is V11() real ext-real Element of REAL
(F,G) . g9 is V11() real ext-real Element of REAL
1 * ((F,G) . g9) is V11() real ext-real Element of REAL
(1 * ((F,G) . g9)) + (1 * ((F,G) . g9)) is V11() real ext-real Element of REAL
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() V78() V80() Element of NAT
(1 + 1) * ((F,G) . g9) is V11() real ext-real Element of REAL
(F,G) . g9 is V11() real ext-real Element of REAL
(F . g9) + (G . g9) is V11() real ext-real Element of REAL
2 * ((F,G) . g9) is V11() real ext-real Element of REAL
f * ((F,G) . g9) is V11() real ext-real Element of REAL
f * (2 * ((F,G) . g9)) is V11() real ext-real Element of REAL
((F,G) . g9) + 0 is V11() real ext-real Element of REAL
((F,G) . g9) + 0 is V11() real ext-real Element of REAL
(G . g9) + (F . g9) is V11() real ext-real Element of REAL
t * ((F,G) . g9) is V11() real ext-real Element of REAL
t * ((F,G) . g9) is V11() real ext-real Element of REAL
f . g9 is V11() real ext-real Element of REAL
2 * f is V11() real ext-real Element of REAL
(2 * f) * ((F,G) . g9) is V11() real ext-real Element of REAL
2 * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional integer finite V59() V66() V67() V68() V69() V70() V71() V72() V73() V80() V81() V82() V83() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
t is V11() real ext-real Element of REAL
f9 is V11() real ext-real Element of REAL
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is V11() real ext-real Element of REAL
f9 is V11() real ext-real Element of REAL
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,f) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (g9,(max (f,f))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . e is V11() real ext-real Element of REAL
G . e is V11() real ext-real Element of REAL
0 + (G . e) is V11() real ext-real Element of REAL
(F . e) + (G . e) is V11() real ext-real Element of REAL
max ((F . e),(G . e)) is V11() real ext-real Element of REAL
1 * (max ((F . e),(G . e))) is V11() real ext-real Element of REAL
(1 * (max ((F . e),(G . e)))) + (1 * (max ((F . e),(G . e)))) is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative Element of REAL
(2 ") * ((F . e) + (G . e)) is V11() real ext-real Element of REAL
2 * (max ((F . e),(G . e))) is V11() real ext-real Element of REAL
(2 ") * (2 * (max ((F . e),(G . e)))) is V11() real ext-real Element of REAL
(F,G) . e is V11() real ext-real Element of REAL
(2 ") * ((F,G) . e) is V11() real ext-real Element of REAL
f9 * ((2 ") * ((F,G) . e)) is V11() real ext-real Element of REAL
f9 * (max ((F . e),(G . e))) is V11() real ext-real Element of REAL
(F,G) . e is V11() real ext-real Element of REAL
f9 * ((F,G) . e) is V11() real ext-real Element of REAL
(F . e) + 0 is V11() real ext-real Element of REAL
t * ((F,G) . e) is V11() real ext-real Element of REAL
t * ((F,G) . e) is V11() real ext-real Element of REAL
t . e is V11() real ext-real Element of REAL
f9 * (2 ") is V11() real ext-real Element of REAL
(f9 * (2 ")) * ((F,G) . e) is V11() real ext-real Element of REAL
f9 * 0 is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
F /" G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
F (#) (G ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
lim (F /" G) is V11() real ext-real Element of REAL
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (G . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) /\ (G) is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
F /" G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
F (#) (G ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
lim (F /" G) is V11() real ext-real Element of REAL
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (G . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) /\ (G) is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () () Element of K6(K7(NAT,REAL))
F /" G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G " is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
F (#) (G ") is V16() V19( NAT ) Function-like V26( NAT ) V33() V34() V35() set
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (G . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(G) /\ (G) is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
G is set
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or not b₄ in G or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
IT1 is set
x is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . x is V11() real ext-real Element of REAL
1 * (F . x) is V11() real ext-real Element of REAL
x is non empty functional set
f is V16() Function-like Element of x
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G is set
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or not b₄ in G or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
IT1 is set
x is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . x is V11() real ext-real Element of REAL
1 * (F . x) is V11() real ext-real Element of REAL
x is non empty functional set
f is V16() Function-like Element of x
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G is set
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂, b₃ being V11() real ext-real Element of REAL ex b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & not b₃ <= 0 & ( for b₅ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₄ <= b₅ or not b₅ in G or ( b₃ * (F . b₅) <= b₁ . b₅ & b₁ . b₅ <= b₂ * (F . b₅) ) ) ) ) } is set
IT1 is set
x is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . IT1 is V11() real ext-real Element of REAL
1 * (F . IT1) is V11() real ext-real Element of REAL
IT1 is non empty functional set
x is V16() Function-like Element of IT1
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V11() real ext-real Element of REAL
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is set
(F,G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂, b₃ being V11() real ext-real Element of REAL ex b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & not b₃ <= 0 & ( for b₅ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₄ <= b₅ or not b₅ in G or ( b₃ * (F . b₅) <= b₁ . b₅ & b₁ . b₅ <= b₂ * (F . b₅) ) ) ) ) } is set
(F,G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or not b₄ in G or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F,G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or not b₄ in G or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(F,G) /\ (F,G) is set
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT is set
x is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (t,IT1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . g9 is V11() real ext-real Element of REAL
f * (F . g9) is V11() real ext-real Element of REAL
x . g9 is V11() real ext-real Element of REAL
f * 0 is V11() real ext-real Element of REAL
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x . g9 is V11() real ext-real Element of REAL
F . g9 is V11() real ext-real Element of REAL
f * (F . g9) is V11() real ext-real Element of REAL
f * (F . g9) is V11() real ext-real Element of REAL
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,t) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . n is V11() real ext-real Element of REAL
t * (F . n) is V11() real ext-real Element of REAL
IT1 . n is V11() real ext-real Element of REAL
f * (F . n) is V11() real ext-real Element of REAL
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT . IT1 is V11() real ext-real Element of REAL
G * IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . (G * IT1) is V11() real ext-real Element of REAL
IT is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
IT1 is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT . x is V11() real ext-real Element of REAL
G * x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . (G * x) is V11() real ext-real Element of REAL
IT1 . x is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(F,G) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,IT) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
log (G,t) is V11() real ext-real Element of REAL
[/(log (G,t))\] is V11() real ext-real integer set
log (G,1) is V11() real ext-real Element of REAL
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G |^ f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . n is V11() real ext-real Element of REAL
1 * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G to_power (log (G,t)) is V11() real ext-real Element of REAL
G to_power f9 is V11() real ext-real Element of REAL
G |^ f9 is set
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
g9 * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . n is V11() real ext-real Element of REAL
x * (F . n) is V11() real ext-real Element of REAL
x * 0 is V11() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G |^ e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(G |^ e) * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . ((G |^ e) * n) is V11() real ext-real Element of REAL
x |^ e is V11() real ext-real Element of REAL
(x |^ e) * (F . n) is V11() real ext-real Element of REAL
e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer V66() V67() V68() V69() V70() V71() V72() V78() V80() Element of NAT
G |^ (e + 1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(G |^ (e + 1)) * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . ((G |^ (e + 1)) * n) is V11() real ext-real Element of REAL
x |^ (e + 1) is V11() real ext-real Element of REAL
(x |^ (e + 1)) * (F . n) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . n is V11() real ext-real Element of REAL
x * (F . n) is V11() real ext-real Element of REAL
x * ((x |^ e) * (F . n)) is V11() real ext-real Element of REAL
x * (x |^ e) is V11() real ext-real Element of REAL
(x * (x |^ e)) * (F . n) is V11() real ext-real Element of REAL
x to_power 1 is V11() real ext-real Element of REAL
x |^ 1 is set
x to_power e is V11() real ext-real Element of REAL
x |^ e is set
(x to_power 1) * (x to_power e) is V11() real ext-real Element of REAL
((x to_power 1) * (x to_power e)) * (F . n) is V11() real ext-real Element of REAL
x to_power (e + 1) is V11() real ext-real Element of REAL
x |^ (e + 1) is set
(x to_power (e + 1)) * (F . n) is V11() real ext-real Element of REAL
G to_power 0 is V11() real ext-real Element of REAL
G |^ 0 is set
(G to_power 0) * n is V11() real ext-real Element of REAL
G to_power e is V11() real ext-real Element of REAL
G |^ e is set
(F,G) . n is V11() real ext-real Element of REAL
G * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . (G * n) is V11() real ext-real Element of REAL
G to_power (e + 1) is V11() real ext-real Element of REAL
G |^ (e + 1) is set
(G to_power (e + 1)) * n is V11() real ext-real Element of REAL
F . ((G to_power (e + 1)) * n) is V11() real ext-real Element of REAL
G to_power 1 is V11() real ext-real Element of REAL
G |^ 1 is set
G to_power e is V11() real ext-real Element of REAL
G |^ e is set
(G to_power 1) * (G to_power e) is V11() real ext-real Element of REAL
((G to_power 1) * (G to_power e)) * n is V11() real ext-real Element of REAL
F . (((G to_power 1) * (G to_power e)) * n) is V11() real ext-real Element of REAL
G * (G |^ e) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(G * (G |^ e)) * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . ((G * (G |^ e)) * n) is V11() real ext-real Element of REAL
G * ((G |^ e) * n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . (G * ((G |^ e) * n)) is V11() real ext-real Element of REAL
G |^ 0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(G |^ 0) * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . ((G |^ 0) * n) is V11() real ext-real Element of REAL
G to_power 0 is V11() real ext-real Element of REAL
G |^ 0 is set
(G to_power 0) * n is V11() real ext-real Element of REAL
F . ((G to_power 0) * n) is V11() real ext-real Element of REAL
F . (1 * n) is V11() real ext-real Element of REAL
1 * (F . n) is V11() real ext-real Element of REAL
x to_power 0 is V11() real ext-real Element of REAL
x |^ 0 is set
(x to_power 0) * (F . n) is V11() real ext-real Element of REAL
x |^ 0 is V11() real ext-real Element of REAL
(x |^ 0) * (F . n) is V11() real ext-real Element of REAL
(G |^ f9) * n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
F . ((G |^ f9) * n) is V11() real ext-real Element of REAL
x |^ f9 is V11() real ext-real Element of REAL
(x |^ f9) * (F . n) is V11() real ext-real Element of REAL
(F,g9) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
(F,g9) . n is V11() real ext-real Element of REAL
F . (t * n) is V11() real ext-real Element of REAL
F . (g9 * n) is V11() real ext-real Element of REAL
(F,t) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
(F,t) . n is V11() real ext-real Element of REAL
x to_power f9 is V11() real ext-real Element of REAL
x |^ f9 is set
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () Element of K6(K7(NAT,REAL))
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
{ (IT |^ b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : verum } is set
(F, { (IT |^ b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : verum } ) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or not b₄ in { (IT |^ b₁) where b₅ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : verum } or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F,IT) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f9 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
g9 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
g9 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,t) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max ((max (f,t)),(max (f,n))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT * (max ((max (f,t)),(max (f,n)))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (1,(IT * (max ((max (f,t)),(max (f,n)))))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (N,(max (1,(IT * (max ((max (f,t)),(max (f,n)))))))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
1 * (max ((max (f,t)),(max (f,n)))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT " is V11() real ext-real non negative Element of REAL
(IT ") * (IT * (max ((max (f,t)),(max (f,n))))) is V11() real ext-real non negative Element of REAL
(max (N,(max (1,(IT * (max ((max (f,t)),(max (f,n))))))))) * (IT ") is V11() real ext-real non negative Element of REAL
(IT ") * IT is V11() real ext-real non negative Element of REAL
((IT ") * IT) * (max ((max (f,t)),(max (f,n)))) is V11() real ext-real non negative Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
log (IT,n) is V11() real ext-real Element of REAL
[\(log (IT,n))/] is V11() real ext-real integer set
IT to_power [\(log (IT,n))/] is V11() real ext-real set
IT to_power (log (IT,n)) is V11() real ext-real Element of REAL
log (IT,1) is V11() real ext-real Element of REAL
(log (IT,n)) - 1 is V11() real ext-real Element of REAL
[\(log (IT,n))/] + 1 is V11() real ext-real integer Element of REAL
1 + ((log (IT,n)) - 1) is V11() real ext-real Element of REAL
1 + (- 1) is V11() real ext-real integer Element of REAL
(1 + (- 1)) + (log (IT,n)) is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT |^ i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT * n2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT to_power 1 is V11() real ext-real Element of REAL
IT |^ 1 is set
(IT to_power 1) * (IT to_power [\(log (IT,n))/]) is V11() real ext-real Element of REAL
IT to_power ([\(log (IT,n))/] + 1) is V11() real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT |^ n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
n * (IT ") is V11() real ext-real non negative Element of REAL
n / IT is V11() real ext-real non negative Element of REAL
IT * (IT to_power [\(log (IT,n))/]) is V11() real ext-real Element of REAL
(IT ") * (IT * (IT to_power [\(log (IT,n))/])) is V11() real ext-real Element of REAL
((IT ") * IT) * (IT to_power [\(log (IT,n))/]) is V11() real ext-real Element of REAL
1 * (IT to_power [\(log (IT,n))/]) is V11() real ext-real Element of REAL
G . (IT * n2) is V11() real ext-real Element of REAL
F . (IT * n2) is V11() real ext-real Element of REAL
g9 * (F . (IT * n2)) is V11() real ext-real Element of REAL
IT1 . n2 is V11() real ext-real Element of REAL
F . n2 is V11() real ext-real Element of REAL
x * (F . n2) is V11() real ext-real Element of REAL
g9 * (x * (F . n2)) is V11() real ext-real Element of REAL
G . n is V11() real ext-real Element of REAL
g9 * x is V11() real ext-real Element of REAL
(g9 * x) * (F . n2) is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
(g9 * x) * (F . n) is V11() real ext-real Element of REAL
x * 0 is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () Element of K6(K7(NAT,REAL))
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
{ (IT |^ b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : verum } is set
(F, { (IT |^ b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : verum } ) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or not b₄ in { (IT |^ b₁) where b₅ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : verum } or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
IT1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
(F,IT) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
x is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
g9 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
n is V11() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
n is V11() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (t,IT1) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,e) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max ((max (t,IT1)),(max (f,e))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT * (max ((max (t,IT1)),(max (f,e)))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (1,(IT * (max ((max (t,IT1)),(max (f,e)))))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (t,(max (1,(IT * (max ((max (t,IT1)),(max (f,e)))))))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
1 * (max ((max (t,IT1)),(max (f,e)))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT " is V11() real ext-real non negative Element of REAL
(IT ") * (IT * (max ((max (t,IT1)),(max (f,e))))) is V11() real ext-real non negative Element of REAL
(max (t,(max (1,(IT * (max ((max (t,IT1)),(max (f,e))))))))) * (IT ") is V11() real ext-real non negative Element of REAL
(IT ") * IT is V11() real ext-real non negative Element of REAL
((IT ") * IT) * (max ((max (t,IT1)),(max (f,e)))) is V11() real ext-real non negative Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
log (IT,n) is V11() real ext-real Element of REAL
[\(log (IT,n))/] is V11() real ext-real integer set
IT to_power [\(log (IT,n))/] is V11() real ext-real set
[\(log (IT,n))/] + 1 is V11() real ext-real integer Element of REAL
IT to_power (log (IT,n)) is V11() real ext-real Element of REAL
log (IT,1) is V11() real ext-real Element of REAL
(log (IT,n)) - 1 is V11() real ext-real Element of REAL
1 + ((log (IT,n)) - 1) is V11() real ext-real Element of REAL
1 + (- 1) is V11() real ext-real integer Element of REAL
(1 + (- 1)) + (log (IT,n)) is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT |^ i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
n * (IT ") is V11() real ext-real non negative Element of REAL
n / IT is V11() real ext-real non negative Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT * n1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT to_power 1 is V11() real ext-real Element of REAL
IT |^ 1 is set
(IT to_power 1) * (IT to_power [\(log (IT,n))/]) is V11() real ext-real Element of REAL
IT to_power ([\(log (IT,n))/] + 1) is V11() real ext-real Element of REAL
IT * (IT to_power [\(log (IT,n))/]) is V11() real ext-real Element of REAL
(IT ") * (IT * (IT to_power [\(log (IT,n))/])) is V11() real ext-real Element of REAL
((IT ") * IT) * (IT to_power [\(log (IT,n))/]) is V11() real ext-real Element of REAL
1 * (IT to_power [\(log (IT,n))/]) is V11() real ext-real Element of REAL
F . n1 is V11() real ext-real Element of REAL
n * (F . n1) is V11() real ext-real Element of REAL
G . n1 is V11() real ext-real Element of REAL
x . n1 is V11() real ext-real Element of REAL
f * (F . n1) is V11() real ext-real Element of REAL
f " is V11() real ext-real Element of REAL
(f ") * (x . n1) is V11() real ext-real Element of REAL
(f ") * (f * (F . n1)) is V11() real ext-real Element of REAL
(f ") * f is V11() real ext-real Element of REAL
((f ") * f) * (F . n1) is V11() real ext-real Element of REAL
1 * (F . n1) is V11() real ext-real Element of REAL
F . (IT * n1) is V11() real ext-real Element of REAL
(f ") * (F . (IT * n1)) is V11() real ext-real Element of REAL
n * ((f ") * (F . (IT * n1))) is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
n * (f ") is V11() real ext-real Element of REAL
(n * (f ")) * (F . n) is V11() real ext-real Element of REAL
(n * (f ")) * (F . (IT * n1)) is V11() real ext-real Element of REAL
G . n is V11() real ext-real Element of REAL
(f ") * 0 is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(F) /\ (F) is set
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () () Element of K6(K7(NAT,REAL))
IT is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
{ (IT |^ b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : verum } is set
(F, { (IT |^ b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : verum } ) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂, b₃ being V11() real ext-real Element of REAL ex b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & not b₃ <= 0 & ( for b₅ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₄ <= b₅ or not b₅ in { (IT |^ b₁) where b₆ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : verum } or ( b₃ * (F . b₅) <= b₁ . b₅ & b₁ . b₅ <= b₂ * (F . b₅) ) ) ) ) } is set
(F, { (IT |^ b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : verum } ) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or not b₄ in { (IT |^ b₁) where b₅ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : verum } or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(F, { (IT |^ b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : verum } ) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or not b₄ in { (IT |^ b₁) where b₅ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : verum } or ( b₂ * (F . b₄) <= b₁ . b₄ & 0 <= b₁ . b₄ ) ) ) ) } is set
(F, { (IT |^ b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : verum } ) /\ (F, { (IT |^ b₁) where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : verum } ) is set
F is non empty set
Funcs (F,REAL) is non empty functional FUNCTION_DOMAIN of F, REAL
G is non empty functional FUNCTION_DOMAIN of F, REAL
IT is non empty functional FUNCTION_DOMAIN of F, REAL
{ b₁ where b₁ is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL) : ex b₂, b₃ being V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL) st
( b₂ in G & b₃ in IT & ( for b₄ being Element of F holds b₁ . b₄ = (b₂ . b₄) + (b₃ . b₄) ) ) } is set
x is set
K7(F,REAL) is V33() V34() V35() set
K6(K7(F,REAL)) is set
f is set
t is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
f is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
t is Element of F
t . t is V11() real ext-real Element of REAL
f . t is V11() real ext-real Element of REAL
(t . t) + (f . t) is V11() real ext-real Element of REAL
t is non empty V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of K6(K7(F,REAL))
f9 is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
x is set
f is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
f is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
t is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
x is non empty functional set
f is V16() Function-like Element of x
f is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
t is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
t is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
F is non empty set
Funcs (F,REAL) is non empty functional FUNCTION_DOMAIN of F, REAL
G is non empty functional FUNCTION_DOMAIN of F, REAL
IT is non empty functional FUNCTION_DOMAIN of F, REAL
{ b₁ where b₁ is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL) : ex b₂, b₃ being V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL) st
( b₂ in G & b₃ in IT & ( for b₄ being Element of F holds b₁ . b₄ = max ((b₂ . b₄),(b₃ . b₄)) ) ) } is set
x is set
K7(F,REAL) is V33() V34() V35() set
K6(K7(F,REAL)) is set
f is set
t is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
f is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
t is Element of F
t . t is V11() real ext-real Element of REAL
f . t is V11() real ext-real Element of REAL
max ((t . t),(f . t)) is V11() real ext-real Element of REAL
t is non empty V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of K6(K7(F,REAL))
f9 is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
x is set
f is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
f is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
t is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
x is non empty functional set
f is V16() Function-like Element of x
f is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
t is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
t is V16() V19(F) V20( REAL ) Function-like V26(F) quasi_total V33() V34() V35() Element of Funcs (F,REAL)
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(NAT,(F),(G)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂, b₃ being V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) st
( b₂ in (F) & b₃ in (G) & ( for b₄ being Element of NAT holds b₁ . b₄ = (b₂ . b₄) + (b₃ . b₄) ) ) } is set
(F,G) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
((F,G)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * ((F,G) . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is set
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f9 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
g9 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
g9 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (t,n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (t,g9) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x . n is V11() real ext-real Element of REAL
f . n is V11() real ext-real Element of REAL
0 + (f . n) is V11() real ext-real Element of REAL
(x . n) + (f . n) is V11() real ext-real Element of REAL
f . n is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
t * (F . n) is V11() real ext-real Element of REAL
0 * t is V11() real ext-real Element of REAL
(F . n) * t is V11() real ext-real Element of REAL
(max (t,g9)) * (F . n) is V11() real ext-real Element of REAL
f9 . n is V11() real ext-real Element of REAL
(f . n) + (f9 . n) is V11() real ext-real Element of REAL
((max (t,g9)) * (F . n)) + (f9 . n) is V11() real ext-real Element of REAL
G . n is V11() real ext-real Element of REAL
g9 * (G . n) is V11() real ext-real Element of REAL
0 * g9 is V11() real ext-real Element of REAL
(G . n) * g9 is V11() real ext-real Element of REAL
(max (t,g9)) * (G . n) is V11() real ext-real Element of REAL
((max (t,g9)) * (F . n)) + ((max (t,g9)) * (G . n)) is V11() real ext-real Element of REAL
(F . n) + (G . n) is V11() real ext-real Element of REAL
(max (t,g9)) * ((F . n) + (G . n)) is V11() real ext-real Element of REAL
(F,G) . n is V11() real ext-real Element of REAL
(max (t,g9)) * ((F,G) . n) is V11() real ext-real Element of REAL
IT1 . n is V11() real ext-real Element of REAL
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,t) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,(max (f,t))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . f9 is V11() real ext-real Element of REAL
F . f9 is V11() real ext-real Element of REAL
x * (F . f9) is V11() real ext-real Element of REAL
(IT1 . f9) - (x * (F . f9)) is V11() real ext-real Element of REAL
f9 is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . g9 is V11() real ext-real Element of REAL
(F,G) . g9 is V11() real ext-real Element of REAL
x * ((F,G) . g9) is V11() real ext-real Element of REAL
G . g9 is V11() real ext-real Element of REAL
0 * (G . g9) is V11() real ext-real Element of REAL
x * (G . g9) is V11() real ext-real Element of REAL
F . g9 is V11() real ext-real Element of REAL
x * (F . g9) is V11() real ext-real Element of REAL
f9 . g9 is V11() real ext-real Element of REAL
F . g9 is V11() real ext-real Element of REAL
x * (F . g9) is V11() real ext-real Element of REAL
(F . g9) + (G . g9) is V11() real ext-real Element of REAL
x * ((F . g9) + (G . g9)) is V11() real ext-real Element of REAL
(x * (F . g9)) + (x * (G . g9)) is V11() real ext-real Element of REAL
(IT1 . g9) - (x * (F . g9)) is V11() real ext-real Element of REAL
0 + (x * (F . g9)) is V11() real ext-real Element of REAL
f9 . g9 is V11() real ext-real Element of REAL
F . g9 is V11() real ext-real Element of REAL
x * (F . g9) is V11() real ext-real Element of REAL
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . g9 is V11() real ext-real Element of REAL
F . g9 is V11() real ext-real Element of REAL
x * (F . g9) is V11() real ext-real Element of REAL
g9 is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . n is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
x * (F . n) is V11() real ext-real Element of REAL
f9 . n is V11() real ext-real Element of REAL
g9 . n is V11() real ext-real Element of REAL
(g9 . n) + (f9 . n) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . n is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
x * (F . n) is V11() real ext-real Element of REAL
g9 . n is V11() real ext-real Element of REAL
f9 . n is V11() real ext-real Element of REAL
(IT1 . n) - (x * (F . n)) is V11() real ext-real Element of REAL
(g9 . n) + (f9 . n) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . n is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
x * (F . n) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . n is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
x * (F . n) is V11() real ext-real Element of REAL
g9 . n is V11() real ext-real Element of REAL
x * (F . n) is V11() real ext-real Element of REAL
g9 . n is V11() real ext-real Element of REAL
x * (F . n) is V11() real ext-real Element of REAL
F is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (F . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
G is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
(G) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * (G . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
(NAT,(F),(G)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂, b₃ being V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) st
( b₂ in (F) & b₃ in (G) & ( for b₄ being Element of NAT holds b₁ . b₄ = max ((b₂ . b₄),(b₃ . b₄)) ) ) } is set
(F,G) is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() () Element of K6(K7(NAT,REAL))
((F,G)) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂ being V11() real ext-real Element of REAL ex b₃ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( not b₂ <= 0 & ( for b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₃ <= b₄ or ( b₁ . b₄ <= b₂ * ((F,G) . b₄) & 0 <= b₁ . b₄ ) ) ) ) } is set
IT is set
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is V11() real ext-real Element of REAL
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f9 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
g9 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
g9 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (g9,t) is V11() real ext-real Element of REAL
max (n,t) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f9 . n is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
g9 * (F . n) is V11() real ext-real Element of REAL
0 * g9 is V11() real ext-real Element of REAL
(F . n) * g9 is V11() real ext-real Element of REAL
(max (g9,t)) * (F . n) is V11() real ext-real Element of REAL
f . n is V11() real ext-real Element of REAL
G . n is V11() real ext-real Element of REAL
t * (G . n) is V11() real ext-real Element of REAL
0 * t is V11() real ext-real Element of REAL
(G . n) * t is V11() real ext-real Element of REAL
(max (g9,t)) * (G . n) is V11() real ext-real Element of REAL
max ((F . n),(G . n)) is V11() real ext-real Element of REAL
(max (g9,t)) * (max ((F . n),(G . n))) is V11() real ext-real Element of REAL
max ((f9 . n),(f . n)) is V11() real ext-real Element of REAL
(F,G) . n is V11() real ext-real Element of REAL
(max (g9,t)) * ((F,G) . n) is V11() real ext-real Element of REAL
IT1 . n is V11() real ext-real Element of REAL
x . n is V11() real ext-real Element of REAL
f . n is V11() real ext-real Element of REAL
max ((x . n),(f . n)) is V11() real ext-real Element of REAL
IT1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
x is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,t) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
max (f,(max (f,t))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G . f9 is V11() real ext-real Element of REAL
F . f9 is V11() real ext-real Element of REAL
IT1 . f9 is V11() real ext-real Element of REAL
f9 is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
g9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
G . g9 is V11() real ext-real Element of REAL
F . g9 is V11() real ext-real Element of REAL
IT1 . g9 is V11() real ext-real Element of REAL
g9 is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f9 . n is V11() real ext-real Element of REAL
IT1 . n is V11() real ext-real Element of REAL
g9 . n is V11() real ext-real Element of REAL
max ((f9 . n),(g9 . n)) is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . n is V11() real ext-real Element of REAL
f9 . n is V11() real ext-real Element of REAL
g9 . n is V11() real ext-real Element of REAL
max ((f9 . n),(g9 . n)) is V11() real ext-real Element of REAL
G . n is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
G . n is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
G . n is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . n is V11() real ext-real Element of REAL
(F,G) . n is V11() real ext-real Element of REAL
x * ((F,G) . n) is V11() real ext-real Element of REAL
G . n is V11() real ext-real Element of REAL
0 * (G . n) is V11() real ext-real Element of REAL
x * (G . n) is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
g9 . n is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
max ((F . n),(G . n)) is V11() real ext-real Element of REAL
g9 . n is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 . n is V11() real ext-real Element of REAL
(F,G) . n is V11() real ext-real Element of REAL
x * ((F,G) . n) is V11() real ext-real Element of REAL
F . n is V11() real ext-real Element of REAL
0 * (F . n) is V11() real ext-real Element of REAL
x * (F . n) is V11() real ext-real Element of REAL
G . n is V11() real ext-real Element of REAL
max ((F . n),(G . n)) is V11() real ext-real Element of REAL
f9 . n is V11() real ext-real Element of REAL
G . n is V11() real ext-real Element of REAL
f9 . n is V11() real ext-real Element of REAL
G . n is V11() real ext-real Element of REAL
F is non empty functional FUNCTION_DOMAIN of NAT , REAL
G is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b₁ where b₁ is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b₂, b₃ being V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) ex b₄ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT st
( b₂ in F & b₃ in G & ( for b₅ being epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT holds
( not b₄ <= b₅ or b₁ . b₅ = (b₂ . b₅) to_power (b₃ . b₅) ) ) ) } is set
IT1 is set
f is set
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
x is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
f . t is V11() real ext-real Element of REAL
x . t is V11() real ext-real Element of REAL
(f . t) to_power (x . t) is V11() real ext-real Element of REAL
t is non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of K6(K7(NAT,REAL))
t is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
t . f9 is V11() real ext-real Element of REAL
f . f9 is V11() real ext-real Element of REAL
x . f9 is V11() real ext-real Element of REAL
(f . f9) to_power (x . f9) is V11() real ext-real Element of REAL
IT1 is set
x is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT
IT1 is non empty functional set
x is V16() Function-like Element of IT1
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
f is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
t is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL)
t is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT