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
F3() is non empty set
F1() is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
F2() is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
{ F4(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : ( F1() <= b1 & b1 <= F2() ) } is set
K6(F3()) is set
{ F4(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : ( F1() <= b1 & b1 <= F2() & S1[b1] ) } is set
F4(F1()) is Element of F3()
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
F4(IT1) is Element of F3()
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
F4(IT1) is Element of F3()
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
F4(IT1) is Element of F3()
F2() is non empty set
F1() is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
{ F3(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : b1 <= F1() } is set
K6(F2()) is set
{ F3(b1) where b1 is 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 <= b1 & b1 <= F1() ) } 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
F3(IT1) is Element of F2()
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
F3(IT1) is Element of F2()
F2() is non empty set
F1() is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer set
{ F3(b1) where b1 is 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 F1() <= b1 } is set
K6(F2()) 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
{ F3(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer V66() V67() V68() V69() V70() V71() V72() V80() Element of NAT : b1 <= 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
F3(f) is Element of F2()
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
F3(f) is Element of F2()
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))
{ b1 where b1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b2 being V11() real ext-real Element of REAL ex b3 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 b2 <= 0 & ( for b4 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 b3 <= b4 or ( b1 . b4 <= b2 * (F . b4) & 0 <= b1 . b4 ) ) ) ) } 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
{ b1 where b1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b2 being V11() real ext-real Element of REAL ex b3 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 b2 <= 0 & ( for b4 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 b3 <= b4 or ( b1 . b4 <= b2 * (G . b4) & 0 <= b1 . b4 ) ) ) ) } 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
{ b1 where b1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b2 being V11() real ext-real Element of REAL ex b3 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 b2 <= 0 & ( for b4 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 b3 <= b4 or ( b1 . b4 <= b2 * (F . b4) & 0 <= b1 . b4 ) ) ) ) } 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
{ H1(b1) where b1 is 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 <= b1 } 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
{ b1 where b1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b2 being V11() real ext-real Element of REAL ex b3 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 b2 <= 0 & ( for b4 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 b3 <= b4 or ( b1 . b4 <= b2 * (F . b4) & 0 <= b1 . b4 ) ) ) ) } 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
{ H2(b1) where b1 is 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 <= b1 & b1 <= 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
{ H1(b1) where b1 is 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 <= b1 & b1 <= 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
{ b1 where b1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b2 being V11() real ext-real Element of REAL ex b3 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 b2 <= 0 & ( for b4 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 b3 <= b4 or ( b1 . b4 <= b2 * ((F,G) . b4) & 0 <= b1 . b4 ) ) ) ) } 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
{ b1 where b1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b2 being V11() real ext-real Element of REAL ex b3 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 b2 <= 0 & ( for b4 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 b3 <= b4 or ( b1 . b4 <= b2 * ((F,G) . b4) & 0 <= b1 . b4 ) ) ) ) } 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
{ b1 where b1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b2 being V11() real ext-real Element of REAL ex b3 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 b2 <= 0 & ( for b4 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 b3 <= b4 or ( b1 . b4 <= b2 * (F . b4) & 0 <= b1 . b4 ) ) ) ) } 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
{ b1 where b1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b2 being V11() real ext-real Element of REAL ex b3 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 b2 <= 0 & ( for b4 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 b3 <= b4 or ( b1 . b4 <= b2 * (G . b4) & 0 <= b1 . b4 ) ) ) ) } is set
(F) is non empty functional FUNCTION_DOMAIN of NAT , REAL
{ b1 where b1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b2 being V11() real ext-real Element of REAL ex b3 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 b2 <= 0 & ( for b4 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 b3 <= b4 or ( b1 . b4 <= b2 * (F . b4) & 0 <= b1 . b4 ) ) ) ) } 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
{ b1 where b1 is V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() Element of Funcs (NAT,REAL) : ex b2 being V11() real ext-real Element of REAL ex b3 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 b2 <= 0 & ( for b4 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 b3 <= b4 or ( b1 . b4 <= b2 * (G . b4) & 0 <= b1 . b4 ) ) ) ) } 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