REAL is non empty V47() V48() V49() V53() V54() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V47() V53() V54() set
RAT is non empty V47() V48() V49() V50() V53() V54() set
INT is non empty V47() V48() V49() V50() V51() V53() V54() set
omega is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() set
K19(omega) is set
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
K19(K19(REAL)) is set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V47() V48() V49() V50() V51() V52() V53() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V47() V48() V49() V50() V51() V52() V53() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
{{},1} is set
K20(COMPLEX,COMPLEX) is complex-valued set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(REAL,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is set
K20(K20(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is V5( RAT ) complex-valued ext-real-valued real-valued set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is V5( RAT ) complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
K20(K20(NAT,NAT),NAT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
K19(K20(K20(NAT,NAT),NAT)) is set
K19(NAT) is set
0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
K19(K20(NAT,NAT)) is set
{0} is V47() V48() V49() V50() V51() V52() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
+infty is non empty non real ext-real positive non negative set
-infty is non empty non real ext-real non positive negative set
s1 is V30() real ext-real set
f is V30() real ext-real set
f - s1 is V30() real ext-real set
r is V30() real ext-real set
r + s1 is V30() real ext-real set
r - 0 is V30() real ext-real Element of REAL
f + 0 is V30() real ext-real Element of REAL
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s1 is V47() V48() V49() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f + r) is V47() V48() V49() Element of K19(REAL)
dom r is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s1 is V47() V48() V49() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) r) is V47() V48() V49() Element of K19(REAL)
dom r is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
s1 is V30() real ext-real set
].-infty,s1.] is V47() V48() V49() set
f is set
[.s1,+infty.[ is V47() V48() V49() set
f is set
].s1,+infty.[ is V47() V48() V49() set
f is set
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 . 0 is V30() real ext-real Element of REAL
(s1 . 0) - 1 is V30() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . f is V30() real ext-real Element of REAL
(s1 . 0) - 0 is V30() real ext-real Element of REAL
s1 . 0 is V30() real ext-real Element of REAL
(s1 . 0) + 1 is V30() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . f is V30() real ext-real Element of REAL
(s1 . 0) + 0 is V30() real ext-real Element of REAL
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s1 is V30() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . f is V30() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . f is V30() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
r + f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . (r + f) is V30() real ext-real Element of REAL
(s1 . (r + f)) - 0 is V30() real ext-real Element of REAL
abs ((s1 . (r + f)) - 0) is V30() real ext-real Element of REAL
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s1 is V30() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . f is V30() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . f is V30() real ext-real Element of REAL
- (s1 . f) is V30() real ext-real Element of REAL
- 0 is V30() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
r + f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . (r + f) is V30() real ext-real Element of REAL
(s1 . (r + f)) - 0 is V30() real ext-real Element of REAL
abs ((s1 . (r + f)) - 0) is V30() real ext-real Element of REAL
- (s1 . (r + f)) is V30() real ext-real Element of REAL
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s1 is V30() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . r is V30() real ext-real Element of REAL
(s1 . r) - (lim s1) is V30() real ext-real Element of REAL
abs ((s1 . r) - (lim s1)) is V30() real ext-real Element of REAL
- ((s1 . r) - (lim s1)) is V30() real ext-real Element of REAL
(lim s1) - (s1 . r) is V30() real ext-real Element of REAL
(lim s1) + (s1 . r) is V30() real ext-real Element of REAL
(lim s1) - (lim s1) is V30() real ext-real Element of REAL
- (lim s1) is V30() real ext-real Element of REAL
abs (- (lim s1)) is V30() real ext-real Element of REAL
abs (lim s1) is V30() real ext-real Element of REAL
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim s1 is V30() real ext-real Element of REAL
(lim s1) / 2 is V30() real ext-real Element of REAL
NAT --> ((lim s1) / 2) is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total complex-valued ext-real-valued real-valued bounded_above bounded_below bounded convergent Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 - f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- f is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
- 1 is V30() real ext-real non positive set
(- 1) (#) f is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
s1 + (- f) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
f . 0 is V30() real ext-real Element of REAL
lim (s1 - f) is V30() real ext-real Element of REAL
((lim s1) / 2) + ((lim s1) / 2) is V30() real ext-real Element of REAL
(((lim s1) / 2) + ((lim s1) / 2)) - ((lim s1) / 2) is V30() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . s is V30() real ext-real Element of REAL
(s1 - f) . s is V30() real ext-real Element of REAL
f . s is V30() real ext-real Element of REAL
(s1 . s) - (f . s) is V30() real ext-real Element of REAL
(s1 . s) - ((lim s1) / 2) is V30() real ext-real Element of REAL
0 + ((lim s1) / 2) is V30() real ext-real Element of REAL
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k + s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . (k + s) is V30() real ext-real Element of REAL
s1 ^\ s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s1
(s1 ^\ s) . k is V30() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k + s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . (k + s) is V30() real ext-real Element of REAL
s1 ^\ s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s1
(s1 ^\ s) . k is V30() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f ^\ s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f
r is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s + s1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . n is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real set
k + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s + g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f ^\ s1) . (s + g) is V30() real ext-real Element of REAL
(s + g) + s1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
r is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s + s1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . n is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real set
k + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s + g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f ^\ s1) . (s + g) is V30() real ext-real Element of REAL
(s + g) + s1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 + f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
r / 2 is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
max (s,k) is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(s1 + f) . g2 is V30() real ext-real Element of REAL
f . g2 is V30() real ext-real Element of REAL
s1 . g2 is V30() real ext-real Element of REAL
(s1 . g2) + (f . g2) is V30() real ext-real Element of REAL
(r / 2) + (r / 2) is V30() real ext-real Element of REAL
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 + f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
s is V30() real ext-real set
r - s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(s1 + f) . n is V30() real ext-real Element of REAL
s1 . n is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
(s1 . n) + (f . n) is V30() real ext-real Element of REAL
(r - s) + s is V30() real ext-real Element of REAL
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 (#) f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
abs r is V30() real ext-real Element of REAL
sqrt (abs r) is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
max (s,k) is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(s1 (#) f) . g2 is V30() real ext-real Element of REAL
f . g2 is V30() real ext-real Element of REAL
s1 . g2 is V30() real ext-real Element of REAL
(s1 . g2) * (f . g2) is V30() real ext-real Element of REAL
(sqrt (abs r)) ^2 is V30() real ext-real Element of REAL
(sqrt (abs r)) * (sqrt (abs r)) is V30() real ext-real set
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 + f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
r / 2 is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
max (s,k) is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(s1 + f) . g2 is V30() real ext-real Element of REAL
f . g2 is V30() real ext-real Element of REAL
s1 . g2 is V30() real ext-real Element of REAL
(r / 2) + (r / 2) is V30() real ext-real Element of REAL
(s1 . g2) + (f . g2) is V30() real ext-real Element of REAL
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 + f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
s is V30() real ext-real set
r - s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(s1 + f) . n is V30() real ext-real Element of REAL
s1 . n is V30() real ext-real Element of REAL
(r - s) + s is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
(s1 . n) + (f . n) is V30() real ext-real Element of REAL
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V30() real ext-real Element of REAL
f (#) s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (f (#) s1) is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
r / f is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f (#) s1) . k is V30() real ext-real Element of REAL
s1 . k is V30() real ext-real Element of REAL
f * (s1 . k) is V30() real ext-real Element of REAL
(r / f) * f is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
r / f is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f (#) s1) . k is V30() real ext-real Element of REAL
s1 . k is V30() real ext-real Element of REAL
(r / f) * f is V30() real ext-real Element of REAL
f * (s1 . k) is V30() real ext-real Element of REAL
r is V30() real ext-real set
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f (#) s1) . s is V30() real ext-real Element of REAL
s1 . s is V30() real ext-real Element of REAL
f * (s1 . s) is V30() real ext-real Element of REAL
(f (#) s1) . 0 is V30() real ext-real Element of REAL
s1 . 0 is V30() real ext-real Element of REAL
f * (s1 . 0) is V30() real ext-real Element of REAL
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V30() real ext-real Element of REAL
f (#) s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng (f (#) s1) is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
r / f is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f (#) s1) . k is V30() real ext-real Element of REAL
s1 . k is V30() real ext-real Element of REAL
(r / f) * f is V30() real ext-real Element of REAL
f * (s1 . k) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
r / f is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f (#) s1) . k is V30() real ext-real Element of REAL
s1 . k is V30() real ext-real Element of REAL
f * (s1 . k) is V30() real ext-real Element of REAL
(r / f) * f is V30() real ext-real Element of REAL
r is V30() real ext-real set
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f (#) s1) . s is V30() real ext-real Element of REAL
s1 . s is V30() real ext-real Element of REAL
f * (s1 . s) is V30() real ext-real Element of REAL
(f (#) s1) . 0 is V30() real ext-real Element of REAL
s1 . 0 is V30() real ext-real Element of REAL
f * (s1 . 0) is V30() real ext-real Element of REAL
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- 1 is V30() real ext-real non positive set
(- 1) (#) s1 is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
- 1 is V30() real ext-real non positive Element of REAL
(- 1) (#) s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 - f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- f is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
- 1 is V30() real ext-real non positive set
(- 1) (#) f is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
s1 + (- f) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
- 1 is V30() real ext-real non positive Element of REAL
(- 1) (#) f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 - f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- f is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
- 1 is V30() real ext-real non positive set
(- 1) (#) f is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
s1 + (- f) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
- 1 is V30() real ext-real non positive Element of REAL
(- 1) (#) f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 + f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 + f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s1 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V30() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s1 . s is V30() real ext-real Element of REAL
incl NAT is V1() V4( NAT ) V5( REAL ) V5( RAT ) V5( INT ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(NAT,REAL))
f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(incl NAT) . f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (incl NAT) is V1() V4( NAT ) V5( REAL ) V5( RAT ) V5( INT ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- 1 is V30() real ext-real non positive set
(- 1) (#) (incl NAT) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(- (incl NAT)) . r is V30() real ext-real V35() V36() Element of REAL
(incl NAT) . r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
- ((incl NAT) . r) is V30() real ext-real Element of REAL
- r is V30() real ext-real Element of REAL
f . r is V30() real ext-real Element of REAL
- 1 is V30() real ext-real non positive Element of REAL
(- 1) (#) (incl NAT) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f (#) r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
abs k is V30() real ext-real Element of REAL
(abs k) / s is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f (#) r) . g2 is V30() real ext-real Element of REAL
f . g2 is V30() real ext-real Element of REAL
r . g2 is V30() real ext-real Element of REAL
(f . g2) * (r . g2) is V30() real ext-real Element of REAL
((abs k) / s) * s is V30() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f (#) r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- 1 is V30() real ext-real non positive Element of REAL
(- 1) (#) f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((- 1) (#) f) (#) r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
(- 1) (#) (((- 1) (#) f) (#) r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) (f (#) r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) ((- 1) (#) (f (#) r)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) * (- 1) is V30() real ext-real non negative Element of REAL
((- 1) * (- 1)) (#) (f (#) r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f (#) r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- 1 is V30() real ext-real non positive Element of REAL
(- 1) (#) f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((- 1) (#) f) (#) ((- 1) (#) r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f (#) ((- 1) (#) r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) (f (#) ((- 1) (#) r)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) (f (#) r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) (#) ((- 1) (#) (f (#) r)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- 1) * (- 1) is V30() real ext-real non negative Element of REAL
((- 1) * (- 1)) (#) (f (#) r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
abs r is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . n is V30() real ext-real Element of REAL
abs (f . n) is V30() real ext-real Element of REAL
(abs f) . n is V30() real ext-real Element of REAL
- r is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . n is V30() real ext-real Element of REAL
abs (f . n) is V30() real ext-real Element of REAL
- (abs (f . n)) is V30() real ext-real Element of REAL
(abs f) . n is V30() real ext-real Element of REAL
- ((abs f) . n) is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V1() V4( NAT ) V5( NAT ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
f * s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f
k is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
r . g2 is V30() real ext-real Element of REAL
s . g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . (s . g2) is V30() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V1() V4( NAT ) V5( NAT ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
f * s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f
k is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
r . g2 is V30() real ext-real Element of REAL
s . g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . (s . g2) is V30() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim r is V30() real ext-real Element of REAL
f (#) r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(lim r) / 2 is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k + s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
r . (k + s) is V30() real ext-real Element of REAL
r ^\ s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of r
(r ^\ s) . k is V30() real ext-real Element of REAL
f ^\ s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f
(f ^\ s) (#) (r ^\ s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) ^\ s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f (#) r
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
r + 1 is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . k is V30() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
r - 1 is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . k is V30() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f ") is V30() real ext-real Element of REAL
r is V30() real ext-real set
r " is V30() real ext-real set
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . n is V30() real ext-real Element of REAL
1 / (r ") is V30() real ext-real Element of REAL
1 / (f . n) is V30() real ext-real Element of REAL
(f . n) " is V30() real ext-real Element of REAL
(f ") . n is V30() real ext-real Element of REAL
((f ") . n) - 0 is V30() real ext-real Element of REAL
abs (((f ") . n) - 0) is V30() real ext-real Element of REAL
r is V30() real ext-real set
- 0 is V30() real ext-real Element of REAL
r " is V30() real ext-real set
- (r ") is V30() real ext-real set
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . n is V30() real ext-real Element of REAL
1 / (f . n) is V30() real ext-real Element of REAL
1 / (- (r ")) is V30() real ext-real Element of REAL
- 1 is V30() real ext-real non positive Element of REAL
(- 1) * (r ") is V30() real ext-real Element of REAL
((- 1) * (r ")) " is V30() real ext-real Element of REAL
(- 1) " is V30() real ext-real non positive Element of REAL
(r ") " is V30() real ext-real set
((- 1) ") * ((r ") ") is V30() real ext-real Element of REAL
0 / (f . n) is V30() real ext-real Element of REAL
abs (1 / (f . n)) is V30() real ext-real Element of REAL
- (1 / (f . n)) is V30() real ext-real Element of REAL
- (abs (1 / (f . n))) is V30() real ext-real Element of REAL
1 * r is V30() real ext-real Element of REAL
- (1 * r) is V30() real ext-real Element of REAL
(f . n) " is V30() real ext-real Element of REAL
abs ((f . n) ") is V30() real ext-real Element of REAL
(f ") . n is V30() real ext-real Element of REAL
((f ") . n) - 0 is V30() real ext-real Element of REAL
abs (((f ") . n) - 0) is V30() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim f is V30() real ext-real Element of REAL
f " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s is V30() real ext-real Element of REAL
abs s is V30() real ext-real Element of REAL
(abs s) + 1 is V30() real ext-real Element of REAL
((abs s) + 1) " is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
max (r,n) is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f ") . g is V30() real ext-real Element of REAL
f . g is V30() real ext-real Element of REAL
(f . g) - 0 is V30() real ext-real Element of REAL
abs ((f . g) - 0) is V30() real ext-real Element of REAL
1 / (f . g) is V30() real ext-real Element of REAL
1 / (((abs s) + 1) ") is V30() real ext-real Element of REAL
(f . g) " is V30() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim f is V30() real ext-real Element of REAL
f " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s is V30() real ext-real Element of REAL
abs s is V30() real ext-real Element of REAL
(abs s) + 1 is V30() real ext-real Element of REAL
((abs s) + 1) " is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
max (r,n) is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f ") . g is V30() real ext-real Element of REAL
f . g is V30() real ext-real Element of REAL
- (f . g) is V30() real ext-real Element of REAL
(f . g) - 0 is V30() real ext-real Element of REAL
abs ((f . g) - 0) is V30() real ext-real Element of REAL
1 / (- (f . g)) is V30() real ext-real Element of REAL
1 / (((abs s) + 1) ") is V30() real ext-real Element of REAL
(- (f . g)) " is V30() real ext-real Element of REAL
(f . g) " is V30() real ext-real Element of REAL
- ((f . g) ") is V30() real ext-real Element of REAL
- ((abs s) + 1) is V30() real ext-real Element of REAL
- (- ((f . g) ")) is V30() real ext-real Element of REAL
- (abs s) is V30() real ext-real Element of REAL
(- (abs s)) - 1 is V30() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim f is V30() real ext-real Element of REAL
f " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . r is V30() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim f is V30() real ext-real Element of REAL
f " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . r is V30() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim f is V30() real ext-real Element of REAL
f " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim f is V30() real ext-real Element of REAL
f " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /" r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r " is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
f (#) (r ") is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set
lim (f /" r) is V30() real ext-real Element of REAL
r " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r ") is V30() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
r . n is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
f is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
r . n is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is set
rng k is V47() V48() V49() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . g2 is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . n is V30() real ext-real Element of REAL
(incl NAT) . n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* k) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* k) . n is V30() real ext-real Element of REAL
((f /* k) . n) - r is V30() real ext-real Element of REAL
abs (((f /* k) . n) - r) is V30() real ext-real Element of REAL
k . n is V30() real ext-real Element of REAL
f . (k . n) is V30() real ext-real Element of REAL
(f . (k . n)) - r is V30() real ext-real Element of REAL
abs ((f . (k . n)) - r) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
k is V30() real ext-real set
n is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . g is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . (s . g) is V30() real ext-real Element of REAL
(f . (s . g)) - r is V30() real ext-real Element of REAL
abs ((f . (s . g)) - r) is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) . g is V30() real ext-real Element of REAL
((f /* s) . g) - r is V30() real ext-real Element of REAL
abs (((f /* s) . g) - r) is V30() real ext-real Element of REAL
lim (f /* s) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
- k is V30() real ext-real Element of REAL
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is set
rng k is V47() V48() V49() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . g2 is V30() real ext-real Element of REAL
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
- g2 is V30() real ext-real Element of REAL
k . g2 is V30() real ext-real Element of REAL
n . g2 is V30() real ext-real Element of REAL
f /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* k) is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* k) . g2 is V30() real ext-real Element of REAL
((f /* k) . g2) - r is V30() real ext-real Element of REAL
abs (((f /* k) . g2) - r) is V30() real ext-real Element of REAL
k . g2 is V30() real ext-real Element of REAL
f . (k . g2) is V30() real ext-real Element of REAL
(f . (k . g2)) - r is V30() real ext-real Element of REAL
abs ((f . (k . g2)) - r) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
k is V30() real ext-real set
n is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . g is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . (s . g) is V30() real ext-real Element of REAL
(f . (s . g)) - r is V30() real ext-real Element of REAL
abs ((f . (s . g)) - r) is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) . g is V30() real ext-real Element of REAL
((f /* s) . g) - r is V30() real ext-real Element of REAL
abs (((f /* s) . g) - r) is V30() real ext-real Element of REAL
lim (f /* s) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is set
rng s is V47() V48() V49() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . n is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . k is V30() real ext-real Element of REAL
(incl NAT) . k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* s) . k is V30() real ext-real Element of REAL
s . k is V30() real ext-real Element of REAL
f . (s . k) is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
r . g is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . (r . g) is V30() real ext-real Element of REAL
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* r) . g is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is set
rng s is V47() V48() V49() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . n is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . k is V30() real ext-real Element of REAL
(incl NAT) . k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* s) . k is V30() real ext-real Element of REAL
s . k is V30() real ext-real Element of REAL
f . (s . k) is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
r . g is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . (r . g) is V30() real ext-real Element of REAL
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* r) . g is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
- s is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is set
rng s is V47() V48() V49() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . n is V30() real ext-real Element of REAL
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
- n is V30() real ext-real Element of REAL
s . n is V30() real ext-real Element of REAL
k . n is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* s) . n is V30() real ext-real Element of REAL
s . n is V30() real ext-real Element of REAL
f . (s . n) is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
r . g is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . (r . g) is V30() real ext-real Element of REAL
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* r) . g is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
- s is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is set
rng s is V47() V48() V49() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . n is V30() real ext-real Element of REAL
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
- n is V30() real ext-real Element of REAL
s . n is V30() real ext-real Element of REAL
k . n is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* s) . n is V30() real ext-real Element of REAL
s . n is V30() real ext-real Element of REAL
f . (s . n) is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
r . g is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . (r . g) is V30() real ext-real Element of REAL
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* r) . g is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (f + r) is V47() V48() V49() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) + (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (f (#) r) is V47() V48() V49() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (f + r) is V47() V48() V49() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) + (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (f (#) r) is V47() V48() V49() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (f + r) is V47() V48() V49() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) + (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (f (#) r) is V47() V48() V49() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (f + r) is V47() V48() V49() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) + (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (f (#) r) is V47() V48() V49() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f + r) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
(s) is V47() V48() V49() Element of K19(REAL)
].s,+infty.[ is V47() V48() V49() set
r | (s) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng k is V47() V48() V49() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
rng (k ^\ n) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
dom r is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (k ^\ n)) + (r /* (k ^\ n)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f + r) /* k) ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f + r) /* k
(s) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
g2 is V30() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . (g + n) is V30() real ext-real Element of REAL
(k ^\ n) . g is V30() real ext-real Element of REAL
r . ((k ^\ n) . g) is V30() real ext-real Element of REAL
(r /* (k ^\ n)) . g is V30() real ext-real Element of REAL
abs g2 is V30() real ext-real Element of REAL
- (abs g2) is V30() real ext-real Element of REAL
g2 - 0 is V30() real ext-real Element of REAL
(- (abs g2)) - 1 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) r) is V47() V48() V49() Element of K19(REAL)
dom r is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
(k) is V47() V48() V49() Element of K19(REAL)
].k,+infty.[ is V47() V48() V49() set
(dom r) /\ (k) is V47() V48() V49() Element of K19(REAL)
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng n is V47() V48() V49() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of n
rng (n ^\ g2) is V47() V48() V49() Element of K19(REAL)
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . (g + g2) is V30() real ext-real Element of REAL
(n ^\ g2) . g is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= k } is set
r . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
r /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
f /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (n ^\ g2)) (#) (r /* (n ^\ g2)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f (#) r) /* n) ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f (#) r) /* n
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f + r) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
halfline s is V47() V48() V49() Element of K19(REAL)
].-infty,s.[ is V47() V48() V49() set
r | (halfline s) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng k is V47() V48() V49() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
rng (k ^\ n) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
dom r is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (k ^\ n)) + (r /* (k ^\ n)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f + r) /* k) ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f + r) /* k
(halfline s) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
g2 is V30() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . (g + n) is V30() real ext-real Element of REAL
(k ^\ n) . g is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not s <= b1 } is set
r . ((k ^\ n) . g) is V30() real ext-real Element of REAL
(r /* (k ^\ n)) . g is V30() real ext-real Element of REAL
abs g2 is V30() real ext-real Element of REAL
- (abs g2) is V30() real ext-real Element of REAL
g2 - 0 is V30() real ext-real Element of REAL
(- (abs g2)) - 1 is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) r) is V47() V48() V49() Element of K19(REAL)
dom r is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
halfline k is V47() V48() V49() Element of K19(REAL)
].-infty,k.[ is V47() V48() V49() set
(dom r) /\ (halfline k) is V47() V48() V49() Element of K19(REAL)
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng n is V47() V48() V49() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of n
rng (n ^\ g2) is V47() V48() V49() Element of K19(REAL)
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . (g + g2) is V30() real ext-real Element of REAL
(n ^\ g2) . g is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not k <= b1 } is set
r . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
r /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
f /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (n ^\ g2)) (#) (r /* (n ^\ g2)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f (#) r) /* n) ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f (#) r) /* n
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
r (#) f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (r (#) f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (f /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) f) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (r (#) f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (f /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) f) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (r (#) f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (f /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) f) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (r (#) f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (f /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) f) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
r (#) f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (r (#) f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (f /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) f) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (r (#) f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (f /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) f) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (r (#) f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (f /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) f) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (r (#) f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r (#) (f /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) f) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
abs f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
dom (abs f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs (f /* r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs f) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
dom (abs f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs (f /* r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs f) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
abs f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
dom (abs f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs (f /* r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs f) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
dom (abs f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs (f /* r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs f) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
(r) is V47() V48() V49() Element of K19(REAL)
].r,+infty.[ is V47() V48() V49() set
f | (r) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
(r) /\ (dom f) is V47() V48() V49() Element of K19(REAL)
k is V30() real ext-real Element of REAL
n is set
f . n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
abs g2 is V30() real ext-real Element of REAL
abs r is V30() real ext-real Element of REAL
(abs g2) + (abs r) is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . m is V30() real ext-real Element of REAL
0 + r is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= r } is set
g2 + 0 is V30() real ext-real Element of REAL
f . g2 is V30() real ext-real Element of REAL
f . (s . m) is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) . m is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
(r) is V47() V48() V49() Element of K19(REAL)
].r,+infty.[ is V47() V48() V49() set
f | (r) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
(r) is V47() V48() V49() Element of K19(REAL)
].r,+infty.[ is V47() V48() V49() set
f | (r) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
(r) /\ (dom f) is V47() V48() V49() Element of K19(REAL)
k is V30() real ext-real Element of REAL
n is set
f . n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
abs g2 is V30() real ext-real Element of REAL
abs r is V30() real ext-real Element of REAL
(abs g2) + (abs r) is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . m is V30() real ext-real Element of REAL
0 + r is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= r } is set
g2 + 0 is V30() real ext-real Element of REAL
f . (s . m) is V30() real ext-real Element of REAL
f . g2 is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) . m is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
(r) is V47() V48() V49() Element of K19(REAL)
].r,+infty.[ is V47() V48() V49() set
f | (r) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
halfline r is V47() V48() V49() Element of K19(REAL)
].-infty,r.[ is V47() V48() V49() set
f | (halfline r) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
(halfline r) /\ (dom f) is V47() V48() V49() Element of K19(REAL)
k is V30() real ext-real Element of REAL
n is set
f . n is V30() real ext-real Element of REAL
abs r is V30() real ext-real Element of REAL
- (abs r) is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
abs g2 is V30() real ext-real Element of REAL
(- (abs r)) - (abs g2) is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . m is V30() real ext-real Element of REAL
r - 0 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not r <= b1 } is set
- (abs g2) is V30() real ext-real Element of REAL
(- (abs g2)) - (abs r) is V30() real ext-real Element of REAL
g2 - 0 is V30() real ext-real Element of REAL
f . g2 is V30() real ext-real Element of REAL
f . (s . m) is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) . m is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
halfline r is V47() V48() V49() Element of K19(REAL)
].-infty,r.[ is V47() V48() V49() set
f | (halfline r) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
halfline r is V47() V48() V49() Element of K19(REAL)
].-infty,r.[ is V47() V48() V49() set
f | (halfline r) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
(halfline r) /\ (dom f) is V47() V48() V49() Element of K19(REAL)
k is V30() real ext-real Element of REAL
n is set
f . n is V30() real ext-real Element of REAL
abs r is V30() real ext-real Element of REAL
- (abs r) is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
abs g2 is V30() real ext-real Element of REAL
(- (abs r)) - (abs g2) is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . m is V30() real ext-real Element of REAL
r - 0 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not r <= b1 } is set
- (abs g2) is V30() real ext-real Element of REAL
(- (abs g2)) - (abs r) is V30() real ext-real Element of REAL
g2 - 0 is V30() real ext-real Element of REAL
f . (s . m) is V30() real ext-real Element of REAL
f . g2 is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) . m is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
halfline r is V47() V48() V49() Element of K19(REAL)
].-infty,r.[ is V47() V48() V49() set
f | (halfline r) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
(s) is V47() V48() V49() Element of K19(REAL)
].s,+infty.[ is V47() V48() V49() set
(dom r) /\ (s) is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (s) is V47() V48() V49() Element of K19(REAL)
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng k is V47() V48() V49() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g2 is set
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
rng (k ^\ n) is V47() V48() V49() Element of K19(REAL)
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(k ^\ n) . g is V30() real ext-real Element of REAL
g + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . (g + n) is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= s } is set
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(k ^\ n) . g2 is V30() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
r /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* k) ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of r /* k
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
(s) is V47() V48() V49() Element of K19(REAL)
].s,+infty.[ is V47() V48() V49() set
(dom r) /\ (s) is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (s) is V47() V48() V49() Element of K19(REAL)
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng k is V47() V48() V49() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g2 is set
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
rng (k ^\ n) is V47() V48() V49() Element of K19(REAL)
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(k ^\ n) . g is V30() real ext-real Element of REAL
g + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . (g + n) is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= s } is set
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(k ^\ n) . g2 is V30() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
r /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* k) ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of r /* k
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
halfline s is V47() V48() V49() Element of K19(REAL)
].-infty,s.[ is V47() V48() V49() set
(dom r) /\ (halfline s) is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (halfline s) is V47() V48() V49() Element of K19(REAL)
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng k is V47() V48() V49() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g2 is set
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
rng (k ^\ n) is V47() V48() V49() Element of K19(REAL)
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(k ^\ n) . g is V30() real ext-real Element of REAL
g + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . (g + n) is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not s <= b1 } is set
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(k ^\ n) . g2 is V30() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
r /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* k) ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of r /* k
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
halfline s is V47() V48() V49() Element of K19(REAL)
].-infty,s.[ is V47() V48() V49() set
(dom r) /\ (halfline s) is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (halfline s) is V47() V48() V49() Element of K19(REAL)
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng k is V47() V48() V49() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g2 is set
k ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of k
rng (k ^\ n) is V47() V48() V49() Element of K19(REAL)
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(k ^\ n) . g is V30() real ext-real Element of REAL
g + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . (g + n) is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not s <= b1 } is set
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(k ^\ n) . g2 is V30() real ext-real Element of REAL
r . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
f . ((k ^\ n) . g2) is V30() real ext-real Element of REAL
r /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
f /* (k ^\ n) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (k ^\ n)) . g2 is V30() real ext-real Element of REAL
r /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* k) ^\ n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of r /* k
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
(dom r) /\ (dom f) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
(s) is V47() V48() V49() Element of K19(REAL)
].s,+infty.[ is V47() V48() V49() set
k is V30() real ext-real Element of REAL
abs k is V30() real ext-real Element of REAL
abs s is V30() real ext-real Element of REAL
(abs k) + (abs s) is V30() real ext-real Element of REAL
n is V30() real ext-real set
g2 is V30() real ext-real Element of REAL
0 + k is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
0 + s is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= s } is set
(dom r) /\ (s) is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (s) is V47() V48() V49() Element of K19(REAL)
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
r . k is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
(dom r) /\ (dom f) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
(s) is V47() V48() V49() Element of K19(REAL)
].s,+infty.[ is V47() V48() V49() set
k is V30() real ext-real Element of REAL
abs k is V30() real ext-real Element of REAL
abs s is V30() real ext-real Element of REAL
(abs k) + (abs s) is V30() real ext-real Element of REAL
n is V30() real ext-real set
g2 is V30() real ext-real Element of REAL
0 + k is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
0 + s is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= s } is set
(dom r) /\ (s) is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (s) is V47() V48() V49() Element of K19(REAL)
k is V30() real ext-real Element of REAL
r . k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
(dom r) /\ (dom f) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
halfline s is V47() V48() V49() Element of K19(REAL)
].-infty,s.[ is V47() V48() V49() set
k is V30() real ext-real Element of REAL
abs k is V30() real ext-real Element of REAL
- (abs k) is V30() real ext-real Element of REAL
abs s is V30() real ext-real Element of REAL
(- (abs k)) - (abs s) is V30() real ext-real Element of REAL
n is V30() real ext-real set
g2 is V30() real ext-real Element of REAL
k - 0 is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
- (abs s) is V30() real ext-real Element of REAL
(- (abs s)) - (abs k) is V30() real ext-real Element of REAL
s - 0 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not s <= b1 } is set
(dom r) /\ (halfline s) is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (halfline s) is V47() V48() V49() Element of K19(REAL)
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
r . k is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
(dom r) /\ (dom f) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
halfline s is V47() V48() V49() Element of K19(REAL)
].-infty,s.[ is V47() V48() V49() set
k is V30() real ext-real Element of REAL
abs k is V30() real ext-real Element of REAL
- (abs k) is V30() real ext-real Element of REAL
abs s is V30() real ext-real Element of REAL
(- (abs k)) - (abs s) is V30() real ext-real Element of REAL
n is V30() real ext-real set
g2 is V30() real ext-real Element of REAL
k - 0 is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
- (abs s) is V30() real ext-real Element of REAL
(- (abs s)) - (abs k) is V30() real ext-real Element of REAL
s - 0 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not s <= b1 } is set
(dom r) /\ (halfline s) is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (halfline s) is V47() V48() V49() Element of K19(REAL)
k is V30() real ext-real Element of REAL
r . k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng k is V47() V48() V49() Element of K19(REAL)
n is V30() real ext-real set
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . g2 is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . n is V30() real ext-real Element of REAL
(incl NAT) . n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* k) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
- n is V30() real ext-real Element of REAL
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng n is V47() V48() V49() Element of K19(REAL)
g2 is V30() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . g is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
- g2 is V30() real ext-real Element of REAL
n . g2 is V30() real ext-real Element of REAL
k . g2 is V30() real ext-real Element of REAL
f /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* n) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
- n is V30() real ext-real Element of REAL
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
g2 is set
rng n is V47() V48() V49() Element of K19(REAL)
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . g is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
- g2 is V30() real ext-real Element of REAL
n . g2 is V30() real ext-real Element of REAL
s . g2 is V30() real ext-real Element of REAL
f /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* n) is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* n) . g2 is V30() real ext-real Element of REAL
((f /* n) . g2) - r is V30() real ext-real Element of REAL
abs (((f /* n) . g2) - r) is V30() real ext-real Element of REAL
n . g2 is V30() real ext-real Element of REAL
f . (n . g2) is V30() real ext-real Element of REAL
(f . (n . g2)) - r is V30() real ext-real Element of REAL
abs ((f . (n . g2)) - r) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
k is V30() real ext-real set
n is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . g is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . (s . g) is V30() real ext-real Element of REAL
(f . (s . g)) - r is V30() real ext-real Element of REAL
abs ((f . (s . g)) - r) is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) . g is V30() real ext-real Element of REAL
((f /* s) . g) - r is V30() real ext-real Element of REAL
abs (((f /* s) . g) - r) is V30() real ext-real Element of REAL
lim (f /* s) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is set
rng k is V47() V48() V49() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . g2 is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . n is V30() real ext-real Element of REAL
(incl NAT) . n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* k) is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* k) . n is V30() real ext-real Element of REAL
((f /* k) . n) - r is V30() real ext-real Element of REAL
abs (((f /* k) . n) - r) is V30() real ext-real Element of REAL
k . n is V30() real ext-real Element of REAL
f . (k . n) is V30() real ext-real Element of REAL
(f . (k . n)) - r is V30() real ext-real Element of REAL
abs ((f . (k . n)) - r) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
k is V30() real ext-real set
n is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . g is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
f . (s . g) is V30() real ext-real Element of REAL
(f . (s . g)) - r is V30() real ext-real Element of REAL
abs ((f . (s . g)) - r) is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) . g is V30() real ext-real Element of REAL
((f /* s) . g) - r is V30() real ext-real Element of REAL
abs (((f /* s) . g) - r) is V30() real ext-real Element of REAL
lim (f /* s) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
r (#) f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((r (#) f)) is V30() real ext-real Element of REAL
r * (f) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (r (#) f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* s) is V30() real ext-real Element of REAL
r (#) (f /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) f) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((r (#) f) /* s) is V30() real ext-real Element of REAL
lim (r (#) (f /* s)) is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- 1 is V30() real ext-real non positive set
(- 1) (#) f is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
((- f)) is V30() real ext-real Element of REAL
(f) is V30() real ext-real Element of REAL
- (f) is V30() real ext-real Element of REAL
- 1 is V30() real ext-real non positive Element of REAL
(- 1) (#) f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(- 1) * (f) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f + r) is V47() V48() V49() Element of K19(REAL)
((f + r)) is V30() real ext-real Element of REAL
(r) is V30() real ext-real Element of REAL
(f) + (r) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
dom r is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* s) is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* s) is V30() real ext-real Element of REAL
(f /* s) + (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f + r) /* s) is V30() real ext-real Element of REAL
lim ((f /* s) + (r /* s)) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f - r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- r is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
- 1 is V30() real ext-real non positive set
(- 1) (#) r is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
f + (- r) is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
dom (f - r) is V47() V48() V49() Element of K19(REAL)
((f - r)) is V30() real ext-real Element of REAL
(r) is V30() real ext-real Element of REAL
(f) - (r) is V30() real ext-real Element of REAL
- r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((- r)) is V30() real ext-real Element of REAL
- (r) is V30() real ext-real Element of REAL
(f) + (- (r)) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f " {0} is V47() V48() V49() Element of K19(REAL)
(f) is V30() real ext-real Element of REAL
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f ^)) is V30() real ext-real Element of REAL
(f) " is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
dom (f ^) is V47() V48() V49() Element of K19(REAL)
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* r) is V30() real ext-real Element of REAL
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
lim ((f /* r) ") is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
abs f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((abs f)) is V30() real ext-real Element of REAL
(f) is V30() real ext-real Element of REAL
abs (f) is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
dom (abs f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* r) is V30() real ext-real Element of REAL
abs (f /* r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs f) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((abs f) /* r) is V30() real ext-real Element of REAL
lim (abs (f /* r)) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f ^)) is V30() real ext-real Element of REAL
(f) " is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
dom (f ^) is V47() V48() V49() Element of K19(REAL)
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* r) is V30() real ext-real Element of REAL
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
lim ((f /* r) ") is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
f . s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) r) is V47() V48() V49() Element of K19(REAL)
((f (#) r)) is V30() real ext-real Element of REAL
(r) is V30() real ext-real Element of REAL
(f) * (r) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
dom r is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* s) is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* s) is V30() real ext-real Element of REAL
(f /* s) (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f (#) r) /* s) is V30() real ext-real Element of REAL
lim ((f /* s) (#) (r /* s)) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(r) is V30() real ext-real Element of REAL
f / r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f / r) is V47() V48() V49() Element of K19(REAL)
((f / r)) is V30() real ext-real Element of REAL
(f) / (r) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
dom r is V47() V48() V49() Element of K19(REAL)
r " {0} is V47() V48() V49() Element of K19(REAL)
(dom r) \ (r " {0}) is V47() V48() V49() Element of K19(REAL)
(dom f) /\ ((dom r) \ (r " {0})) is V47() V48() V49() Element of K19(REAL)
r ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (r ^) is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom (r ^)) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
r . n is V30() real ext-real Element of REAL
((r ^)) is V30() real ext-real Element of REAL
(r) " is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f (#) (r ^) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) (r ^)) is V47() V48() V49() Element of K19(REAL)
((f (#) (r ^))) is V30() real ext-real Element of REAL
(f) * ((r) ") is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
r (#) f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((r (#) f)) is V30() real ext-real Element of REAL
r * (f) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom (r (#) f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* s) is V30() real ext-real Element of REAL
r (#) (f /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r (#) f) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((r (#) f) /* s) is V30() real ext-real Element of REAL
lim (r (#) (f /* s)) is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- 1 is V30() real ext-real non positive set
(- 1) (#) f is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
((- f)) is V30() real ext-real Element of REAL
(f) is V30() real ext-real Element of REAL
- (f) is V30() real ext-real Element of REAL
- 1 is V30() real ext-real non positive Element of REAL
(- 1) (#) f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(- 1) * (f) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f + r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f + r) is V47() V48() V49() Element of K19(REAL)
((f + r)) is V30() real ext-real Element of REAL
(r) is V30() real ext-real Element of REAL
(f) + (r) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
dom r is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* s) is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* s) is V30() real ext-real Element of REAL
(f /* s) + (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f + r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f + r) /* s) is V30() real ext-real Element of REAL
lim ((f /* s) + (r /* s)) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f - r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- r is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
- 1 is V30() real ext-real non positive set
(- 1) (#) r is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
f + (- r) is V1() V4( REAL ) V6() complex-valued ext-real-valued real-valued set
dom (f - r) is V47() V48() V49() Element of K19(REAL)
((f - r)) is V30() real ext-real Element of REAL
(r) is V30() real ext-real Element of REAL
(f) - (r) is V30() real ext-real Element of REAL
- r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((- r)) is V30() real ext-real Element of REAL
- (r) is V30() real ext-real Element of REAL
(f) + (- (r)) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f " {0} is V47() V48() V49() Element of K19(REAL)
(f) is V30() real ext-real Element of REAL
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f ^)) is V30() real ext-real Element of REAL
(f) " is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
dom (f ^) is V47() V48() V49() Element of K19(REAL)
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* r) is V30() real ext-real Element of REAL
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
lim ((f /* r) ") is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
abs f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((abs f)) is V30() real ext-real Element of REAL
(f) is V30() real ext-real Element of REAL
abs (f) is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
dom (abs f) is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* r) is V30() real ext-real Element of REAL
abs (f /* r) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(abs f) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((abs f) /* r) is V30() real ext-real Element of REAL
lim (abs (f /* r)) is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f ^)) is V30() real ext-real Element of REAL
(f) " is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
dom (f ^) is V47() V48() V49() Element of K19(REAL)
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* r) is V30() real ext-real Element of REAL
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
lim ((f /* r) ") is V30() real ext-real Element of REAL
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
f . s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) r) is V47() V48() V49() Element of K19(REAL)
((f (#) r)) is V30() real ext-real Element of REAL
(r) is V30() real ext-real Element of REAL
(f) * (r) is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
dom f is V47() V48() V49() Element of K19(REAL)
dom r is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
r /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* s) is V30() real ext-real Element of REAL
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* s) is V30() real ext-real Element of REAL
(f /* s) (#) (r /* s) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f (#) r) /* s) is V30() real ext-real Element of REAL
lim ((f /* s) (#) (r /* s)) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(r) is V30() real ext-real Element of REAL
f / r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f / r) is V47() V48() V49() Element of K19(REAL)
((f / r)) is V30() real ext-real Element of REAL
(f) / (r) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
dom r is V47() V48() V49() Element of K19(REAL)
r " {0} is V47() V48() V49() Element of K19(REAL)
(dom r) \ (r " {0}) is V47() V48() V49() Element of K19(REAL)
(dom f) /\ ((dom r) \ (r " {0})) is V47() V48() V49() Element of K19(REAL)
r ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (r ^) is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom (r ^)) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
r . n is V30() real ext-real Element of REAL
((r ^)) is V30() real ext-real Element of REAL
(r) " is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f (#) (r ^) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) (r ^)) is V47() V48() V49() Element of K19(REAL)
((f (#) (r ^))) is V30() real ext-real Element of REAL
(f) * ((r) ") is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) r) is V47() V48() V49() Element of K19(REAL)
((f (#) r)) is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
(s) is V47() V48() V49() Element of K19(REAL)
].s,+infty.[ is V47() V48() V49() set
r | (s) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
(s) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
k is V30() real ext-real set
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng n is V47() V48() V49() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of n
rng (n ^\ g2) is V47() V48() V49() Element of K19(REAL)
abs k is V30() real ext-real Element of REAL
(abs k) + 1 is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . (g + g2) is V30() real ext-real Element of REAL
(n ^\ g2) . g is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= s } is set
r . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
abs (r . ((n ^\ g2) . g)) is V30() real ext-real Element of REAL
r /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
abs ((r /* (n ^\ g2)) . g) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
f /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (n ^\ g2)) (#) (r /* (n ^\ g2)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f (#) r) /* n) ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f (#) r) /* n
lim (f /* (n ^\ g2)) is V30() real ext-real Element of REAL
lim ((f /* (n ^\ g2)) (#) (r /* (n ^\ g2))) is V30() real ext-real Element of REAL
lim ((f (#) r) /* n) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f (#) r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (f (#) r) is V47() V48() V49() Element of K19(REAL)
((f (#) r)) is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
halfline s is V47() V48() V49() Element of K19(REAL)
].-infty,s.[ is V47() V48() V49() set
r | (halfline s) is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
(halfline s) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
k is V30() real ext-real set
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng n is V47() V48() V49() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of n
rng (n ^\ g2) is V47() V48() V49() Element of K19(REAL)
abs k is V30() real ext-real Element of REAL
(abs k) + 1 is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
g + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . (g + g2) is V30() real ext-real Element of REAL
(n ^\ g2) . g is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not s <= b1 } is set
r . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
abs (r . ((n ^\ g2) . g)) is V30() real ext-real Element of REAL
r /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
abs ((r /* (n ^\ g2)) . g) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
f /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (n ^\ g2)) (#) (r /* (n ^\ g2)) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f (#) r) /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f (#) r) /* n) ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f (#) r) /* n
lim (f /* (n ^\ g2)) is V30() real ext-real Element of REAL
lim ((f /* (n ^\ g2)) (#) (r /* (n ^\ g2))) is V30() real ext-real Element of REAL
lim ((f (#) r) /* n) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(r) is V30() real ext-real Element of REAL
dom r is V47() V48() V49() Element of K19(REAL)
s is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom s is V47() V48() V49() Element of K19(REAL)
(s) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
(k) is V47() V48() V49() Element of K19(REAL)
].k,+infty.[ is V47() V48() V49() set
(dom f) /\ (k) is V47() V48() V49() Element of K19(REAL)
(dom r) /\ (k) is V47() V48() V49() Element of K19(REAL)
(dom s) /\ (k) is V47() V48() V49() Element of K19(REAL)
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng n is V47() V48() V49() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of n
g is set
rng (n ^\ g2) is V47() V48() V49() Element of K19(REAL)
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(n ^\ g2) . g is V30() real ext-real Element of REAL
g + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . (g + g2) is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= k } is set
r /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* (n ^\ g2)) is V30() real ext-real Element of REAL
f /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (n ^\ g2)) is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(n ^\ g2) . g is V30() real ext-real Element of REAL
s . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
r . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
s /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
f . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
(f /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
(r /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
s /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* n) ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s /* n
lim ((s /* n) ^\ g2) is V30() real ext-real Element of REAL
lim (s /* n) is V30() real ext-real Element of REAL
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng n is V47() V48() V49() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of n
g is set
rng (n ^\ g2) is V47() V48() V49() Element of K19(REAL)
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(n ^\ g2) . g is V30() real ext-real Element of REAL
g + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . (g + g2) is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= k } is set
f /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (n ^\ g2)) is V30() real ext-real Element of REAL
r /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* (n ^\ g2)) is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(n ^\ g2) . g is V30() real ext-real Element of REAL
s . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
r . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
s /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
f . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
(f /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
(r /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
s /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* n) ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s /* n
lim ((s /* n) ^\ g2) is V30() real ext-real Element of REAL
lim (s /* n) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(r) is V30() real ext-real Element of REAL
dom r is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
s is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom s is V47() V48() V49() Element of K19(REAL)
((dom f) /\ (dom r)) /\ (dom s) is V47() V48() V49() Element of K19(REAL)
(s) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
(k) is V47() V48() V49() Element of K19(REAL)
].k,+infty.[ is V47() V48() V49() set
n is V30() real ext-real Element of REAL
abs n is V30() real ext-real Element of REAL
abs k is V30() real ext-real Element of REAL
(abs n) + (abs k) is V30() real ext-real Element of REAL
g2 is V30() real ext-real set
g is V30() real ext-real Element of REAL
n + 0 is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
0 + k is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= k } is set
(dom f) /\ (k) is V47() V48() V49() Element of K19(REAL)
(dom r) /\ (k) is V47() V48() V49() Element of K19(REAL)
(dom s) /\ (k) is V47() V48() V49() Element of K19(REAL)
n is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
s . n is V30() real ext-real Element of REAL
r . n is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(r) is V30() real ext-real Element of REAL
dom r is V47() V48() V49() Element of K19(REAL)
s is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom s is V47() V48() V49() Element of K19(REAL)
(s) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
halfline k is V47() V48() V49() Element of K19(REAL)
].-infty,k.[ is V47() V48() V49() set
(dom f) /\ (halfline k) is V47() V48() V49() Element of K19(REAL)
(dom r) /\ (halfline k) is V47() V48() V49() Element of K19(REAL)
(dom s) /\ (halfline k) is V47() V48() V49() Element of K19(REAL)
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng n is V47() V48() V49() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of n
g is set
rng (n ^\ g2) is V47() V48() V49() Element of K19(REAL)
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(n ^\ g2) . g is V30() real ext-real Element of REAL
g + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . (g + g2) is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not k <= b1 } is set
r /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* (n ^\ g2)) is V30() real ext-real Element of REAL
f /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (n ^\ g2)) is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(n ^\ g2) . g is V30() real ext-real Element of REAL
s . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
r . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
s /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
f . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
(f /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
(r /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
s /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* n) ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s /* n
lim ((s /* n) ^\ g2) is V30() real ext-real Element of REAL
lim (s /* n) is V30() real ext-real Element of REAL
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng n is V47() V48() V49() Element of K19(REAL)
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of n
g is set
rng (n ^\ g2) is V47() V48() V49() Element of K19(REAL)
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(n ^\ g2) . g is V30() real ext-real Element of REAL
g + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . (g + g2) is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not k <= b1 } is set
f /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* (n ^\ g2)) is V30() real ext-real Element of REAL
r /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* (n ^\ g2)) is V30() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(n ^\ g2) . g is V30() real ext-real Element of REAL
s . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
r . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
s /* (n ^\ g2) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
f . ((n ^\ g2) . g) is V30() real ext-real Element of REAL
(f /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
(r /* (n ^\ g2)) . g is V30() real ext-real Element of REAL
s /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s /* n) ^\ g2 is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s /* n
lim ((s /* n) ^\ g2) is V30() real ext-real Element of REAL
lim (s /* n) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(r) is V30() real ext-real Element of REAL
dom r is V47() V48() V49() Element of K19(REAL)
(dom f) /\ (dom r) is V47() V48() V49() Element of K19(REAL)
s is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom s is V47() V48() V49() Element of K19(REAL)
((dom f) /\ (dom r)) /\ (dom s) is V47() V48() V49() Element of K19(REAL)
(s) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
halfline k is V47() V48() V49() Element of K19(REAL)
].-infty,k.[ is V47() V48() V49() set
n is V30() real ext-real Element of REAL
abs n is V30() real ext-real Element of REAL
- (abs n) is V30() real ext-real Element of REAL
abs k is V30() real ext-real Element of REAL
(- (abs n)) - (abs k) is V30() real ext-real Element of REAL
g2 is V30() real ext-real set
g is V30() real ext-real Element of REAL
n - 0 is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
- (abs k) is V30() real ext-real Element of REAL
(- (abs k)) - (abs n) is V30() real ext-real Element of REAL
k - 0 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not k <= b1 } is set
(dom f) /\ (halfline k) is V47() V48() V49() Element of K19(REAL)
(dom r) /\ (halfline k) is V47() V48() V49() Element of K19(REAL)
(dom s) /\ (halfline k) is V47() V48() V49() Element of K19(REAL)
n is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
s . n is V30() real ext-real Element of REAL
r . n is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
(f) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
(r) is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
(s) is V47() V48() V49() Element of K19(REAL)
].s,+infty.[ is V47() V48() V49() set
(dom f) /\ (s) is V47() V48() V49() Element of K19(REAL)
(dom r) /\ (s) is V47() V48() V49() Element of K19(REAL)
abs s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k + 0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k + (abs s) is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
0 + s is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= s } is set
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . n is V30() real ext-real Element of REAL
(incl NAT) . n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
rng k is V47() V48() V49() Element of K19(REAL)
n is V30() real ext-real set
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . g2 is V30() real ext-real Element of REAL
r /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* k) is V30() real ext-real Element of REAL
n is V30() real ext-real set
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . g2 is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . n is V30() real ext-real Element of REAL
f . (k . n) is V30() real ext-real Element of REAL
r . (k . n) is V30() real ext-real Element of REAL
f /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* k) . n is V30() real ext-real Element of REAL
(r /* k) . n is V30() real ext-real Element of REAL
lim (f /* k) is V30() real ext-real Element of REAL
abs s is V30() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k + 0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k + (abs s) is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
0 + s is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= s } is set
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . n is V30() real ext-real Element of REAL
(incl NAT) . n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
rng k is V47() V48() V49() Element of K19(REAL)
n is V30() real ext-real set
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . g2 is V30() real ext-real Element of REAL
f /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* k) is V30() real ext-real Element of REAL
n is V30() real ext-real set
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . g2 is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
k . n is V30() real ext-real Element of REAL
f . (k . n) is V30() real ext-real Element of REAL
r . (k . n) is V30() real ext-real Element of REAL
(f /* k) . n is V30() real ext-real Element of REAL
r /* k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* k) . n is V30() real ext-real Element of REAL
lim (r /* k) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
r . k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
r . n is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
(f) is V30() real ext-real Element of REAL
r is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom r is V47() V48() V49() Element of K19(REAL)
(r) is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
halfline s is V47() V48() V49() Element of K19(REAL)
].-infty,s.[ is V47() V48() V49() set
(dom f) /\ (halfline s) is V47() V48() V49() Element of K19(REAL)
(dom r) /\ (halfline s) is V47() V48() V49() Element of K19(REAL)
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs s is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
- n is V30() real ext-real Element of REAL
(- n) - (abs s) is V30() real ext-real Element of REAL
(- n) - 0 is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
- (abs s) is V30() real ext-real Element of REAL
(- (abs s)) - n is V30() real ext-real Element of REAL
s - 0 is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not s <= b1 } is set
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
- g2 is V30() real ext-real Element of REAL
n . g2 is V30() real ext-real Element of REAL
k . g2 is V30() real ext-real Element of REAL
rng n is V47() V48() V49() Element of K19(REAL)
g2 is V30() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . g is V30() real ext-real Element of REAL
r /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (r /* n) is V30() real ext-real Element of REAL
g2 is V30() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . g is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . g2 is V30() real ext-real Element of REAL
f . (n . g2) is V30() real ext-real Element of REAL
r . (n . g2) is V30() real ext-real Element of REAL
f /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* n) . g2 is V30() real ext-real Element of REAL
(r /* n) . g2 is V30() real ext-real Element of REAL
lim (f /* n) is V30() real ext-real Element of REAL
k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
abs s is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
- n is V30() real ext-real Element of REAL
(- n) - (abs s) is V30() real ext-real Element of REAL
(- n) - 0 is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
- (abs s) is V30() real ext-real Element of REAL
(- (abs s)) - n is V30() real ext-real Element of REAL
s - 0 is V30() real ext-real Element of REAL
g is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not s <= b1 } is set
n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
- g2 is V30() real ext-real Element of REAL
n . g2 is V30() real ext-real Element of REAL
k . g2 is V30() real ext-real Element of REAL
rng n is V47() V48() V49() Element of K19(REAL)
g2 is V30() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . g is V30() real ext-real Element of REAL
f /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim (f /* n) is V30() real ext-real Element of REAL
g2 is V30() real ext-real set
g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . g is V30() real ext-real Element of REAL
g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n . g2 is V30() real ext-real Element of REAL
f . (n . g2) is V30() real ext-real Element of REAL
r . (n . g2) is V30() real ext-real Element of REAL
(f /* n) . g2 is V30() real ext-real Element of REAL
r /* n is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(r /* n) . g2 is V30() real ext-real Element of REAL
lim (r /* n) is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
r . k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
f . n is V30() real ext-real Element of REAL
r . n is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f ^)) is V30() real ext-real Element of REAL
dom (f ^) is V47() V48() V49() Element of K19(REAL)
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
f . s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f /* r) ") is V30() real ext-real Element of REAL
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f /* r) ") is V30() real ext-real Element of REAL
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V47() V48() V49() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f ^)) is V30() real ext-real Element of REAL
dom (f ^) is V47() V48() V49() Element of K19(REAL)
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
r is V30() real ext-real Element of REAL
s is V30() real ext-real Element of REAL
f . s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f /* r) ") is V30() real ext-real Element of REAL
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng r is V47() V48() V49() Element of K19(REAL)
f /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* r) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f /* r) ") is V30() real ext-real Element of REAL
(f ^) /* r is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((f ^) /* r) is V30() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
(r) is V47() V48() V49() Element of K19(REAL)
].r,+infty.[ is V47() V48() V49() set
(dom f) /\ (r) is V47() V48() V49() Element of K19(REAL)
dom (f ^) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
rng (s ^\ k) is V47() V48() V49() Element of K19(REAL)
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= r } is set
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
(r) is V47() V48() V49() Element of K19(REAL)
].r,+infty.[ is V47() V48() V49() set
(dom f) /\ (r) is V47() V48() V49() Element of K19(REAL)
dom (f ^) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
rng (s ^\ k) is V47() V48() V49() Element of K19(REAL)
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= r } is set
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
halfline r is V47() V48() V49() Element of K19(REAL)
].-infty,r.[ is V47() V48() V49() set
(dom f) /\ (halfline r) is V47() V48() V49() Element of K19(REAL)
dom (f ^) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
rng (s ^\ k) is V47() V48() V49() Element of K19(REAL)
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not r <= b1 } is set
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
halfline r is V47() V48() V49() Element of K19(REAL)
].-infty,r.[ is V47() V48() V49() set
(dom f) /\ (halfline r) is V47() V48() V49() Element of K19(REAL)
dom (f ^) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
f . k is V30() real ext-real Element of REAL
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
rng (s ^\ k) is V47() V48() V49() Element of K19(REAL)
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not r <= b1 } is set
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
(r) is V47() V48() V49() Element of K19(REAL)
].r,+infty.[ is V47() V48() V49() set
(dom f) /\ (r) is V47() V48() V49() Element of K19(REAL)
dom (f ^) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= r } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= r } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
n is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
rng (s ^\ k) is V47() V48() V49() Element of K19(REAL)
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= r } is set
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
(r) is V47() V48() V49() Element of K19(REAL)
].r,+infty.[ is V47() V48() V49() set
(dom f) /\ (r) is V47() V48() V49() Element of K19(REAL)
dom (f ^) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= r } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= r } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
n is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
rng (s ^\ k) is V47() V48() V49() Element of K19(REAL)
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not b1 <= r } is set
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
halfline r is V47() V48() V49() Element of K19(REAL)
].-infty,r.[ is V47() V48() V49() set
(dom f) /\ (halfline r) is V47() V48() V49() Element of K19(REAL)
dom (f ^) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not r <= b1 } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not r <= b1 } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
n is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
rng (s ^\ k) is V47() V48() V49() Element of K19(REAL)
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not r <= b1 } is set
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s
f is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f) is V30() real ext-real Element of REAL
dom f is V47() V48() V49() Element of K19(REAL)
f ^ is V1() V4( REAL ) V5( REAL ) V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
r is V30() real ext-real Element of REAL
halfline r is V47() V48() V49() Element of K19(REAL)
].-infty,r.[ is V47() V48() V49() set
(dom f) /\ (halfline r) is V47() V48() V49() Element of K19(REAL)
dom (f ^) is V47() V48() V49() Element of K19(REAL)
s is V30() real ext-real Element of REAL
k is V30() real ext-real Element of REAL
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not r <= b1 } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
n is V30() real ext-real Element of REAL
g2 is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not r <= b1 } is set
f . g2 is V30() real ext-real Element of REAL
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
n is V30() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng s is V47() V48() V49() Element of K19(REAL)
(f ^) /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of s
rng (s ^\ k) is V47() V48() V49() Element of K19(REAL)
f " {0} is V47() V48() V49() Element of K19(REAL)
(dom f) \ (f " {0}) is V47() V48() V49() Element of K19(REAL)
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
n + k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
s . (n + k) is V30() real ext-real Element of REAL
(s ^\ k) . n is V30() real ext-real Element of REAL
{ b1 where b1 is V30() real ext-real Element of REAL : not r <= b1 } is set
f . ((s ^\ k) . n) is V30() real ext-real Element of REAL
f /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() V36() V47() V48() V49() V50() V51() V52() Element of NAT
(f /* (s ^\ k)) . n is V30() real ext-real Element of REAL
lim (f /* (s ^\ k)) is V30() real ext-real Element of REAL
(f /* (s ^\ k)) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
f /* s is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of f /* s
((f /* s) ^\ k) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(f /* s) " is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((f /* s) ") ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f /* s) "
((f ^) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of (f ^) /* s