:: 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

- 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

{ 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

F4(IT1) is Element of F3()

F4(IT1) is Element of F3()
IT is set

F4(IT1) is Element of F3()
F2() is non empty 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

F3(IT1) is Element of F2()

F3(IT1) is Element of F2()
F2() is non empty 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 + 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

{ 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

F3(f) is Element of F2()

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))

F . G is V11() real ext-real Element of REAL

F . G is V11() real ext-real Element of REAL

F . G is V11() real ext-real Element of REAL

F . G is V11() real ext-real Element of REAL

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))

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))

F . IT is V11() real ext-real Element of REAL

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))

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

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

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 + 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

(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

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) . 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
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

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) . 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
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

(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) . 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

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))

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))

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))

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))

(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))

(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

(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))

F . IT is V11() real ext-real Element of REAL

F . IT1 is V11() real ext-real Element of REAL

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

(abs (lim (F /" G))) * (abs (lim (F /" G))) is V11() real ext-real Element of REAL

((abs (lim (F /" G))) * (abs (lim (F /" G)))) / 2 is V11() real ext-real Element of REAL

(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

((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

(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

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))

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

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

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

(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 . 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

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

x is V11() real ext-real Element of 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))
IT1 . t 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 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

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

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
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)

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

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

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

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))

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

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

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)

{ 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

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

F . n is V11() real ext-real Element of REAL

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

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

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

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

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

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

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

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

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

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

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

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

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

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