:: LIMFUNC2 semantic presentation

REAL is non empty V51() V71() V72() V73() V77() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() Element of K19(REAL)

K19(REAL) is set

COMPLEX is non empty V51() V71() V77() set

omega is non empty epsilon-transitive epsilon-connected ordinal V71() V72() V73() V74() V75() V76() V77() 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 empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V71() V72() V73() V74() V75() V76() V77() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

{{},1} is non empty V71() V72() V73() V74() V75() V76() set

INT is non empty V51() V71() V72() V73() V74() V75() V77() set

RAT is non empty V51() V71() V72() V73() V74() V77() 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 empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V71() V72() V73() V74() V75() V76() V77() V87() V88() Element of NAT

{0} is non empty V71() V72() V73() V74() V75() V76() set

-infty is non empty non real ext-real non positive negative set

+infty is non empty non real ext-real positive non negative set

f is V30() real ext-real set

x0 is V30() real ext-real set

r is V30() real ext-real set

x0 - f is V30() real ext-real set

r + f is V30() real ext-real set

r - 0 is V30() real ext-real Element of REAL

x0 + 0 is V30() real ext-real Element of REAL

x0 is 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 x0 is V71() V72() V73() 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 V71() V72() V73() 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 V71() V72() V73() Element of K19(REAL)

dom r is V71() V72() V73() Element of K19(REAL)

(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)

s is V71() V72() V73() Element of K19(REAL)

(dom (f (#) r)) /\ s is V71() V72() V73() Element of K19(REAL)

(dom f) /\ s is V71() V72() V73() Element of K19(REAL)

(dom r) /\ s is V71() V72() V73() Element of K19(REAL)

x0 is V30() real ext-real Element of REAL

f is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

1 / (f + 1) is V30() real ext-real non negative Element of REAL

x0 - (1 / (f + 1)) is V30() real ext-real Element of REAL

x0 + (1 / (f + 1)) is V30() real ext-real Element of REAL

x0 is 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 x0 is V71() V72() V73() 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 V71() V72() V73() 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 V71() V72() V73() Element of K19(REAL)

dom r is V71() V72() V73() Element of K19(REAL)

(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)

s is V71() V72() V73() Element of K19(REAL)

(dom (f + r)) /\ s is V71() V72() V73() Element of K19(REAL)

(dom f) /\ s is V71() V72() V73() Element of K19(REAL)

(dom r) /\ s is V71() V72() V73() Element of K19(REAL)

x0 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

NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total T-Sequence-like complex-valued ext-real-valued real-valued convergent 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

- 1 is V30() real ext-real non positive set

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

r . 0 is V30() real ext-real Element of REAL

lim r is V30() real ext-real Element of REAL

lim (f - r) is V30() real ext-real Element of REAL

(lim f) - x0 is V30() real ext-real Element of REAL

s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

f . k is V30() real ext-real Element of REAL

(f - r) . k is V30() real ext-real Element of REAL

r . k is V30() real ext-real Element of REAL

(f . k) - (r . k) is V30() real ext-real Element of REAL

(f . k) - x0 is V30() real ext-real Element of REAL

0 + x0 is V30() real ext-real Element of REAL

x0 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

NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total T-Sequence-like complex-valued ext-real-valued real-valued convergent 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))

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

- 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

r + (- f) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set

r . 0 is V30() real ext-real Element of REAL

lim r is V30() real ext-real Element of REAL

lim (r - f) is V30() real ext-real Element of REAL

x0 - (lim f) is V30() real ext-real Element of REAL

s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

f . k is V30() real ext-real Element of REAL

(r - f) . k is V30() real ext-real Element of REAL

r . k is V30() real ext-real Element of REAL

(r . k) - (f . k) is V30() real ext-real Element of REAL

x0 - (f . k) is V30() real ext-real Element of REAL

0 + (f . k) is V30() real ext-real Element of REAL

x0 is V30() real ext-real Element of REAL

right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(x0,+infty) is set

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

rng f is V71() V72() V73() 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 V71() V72() V73() Element of K19(REAL)

(dom r) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)

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

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 non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

f . n is V30() real ext-real Element of REAL

{ b

r . (f . n) is V30() real ext-real Element of REAL

g is V30() real ext-real Element of REAL

(r /* f) . n is V30() real ext-real Element of REAL

x0 is V30() real ext-real Element of REAL

f is V30() real ext-real Element of REAL

f - x0 is V30() real ext-real Element of REAL

].(f - x0),f.[ is V71() V72() V73() 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 V71() V72() V73() Element of K19(REAL)

s is V30() real ext-real Element of REAL

k is V30() real ext-real set

n is V30() real ext-real Element of REAL

g2 is V30() real ext-real Element of REAL

{ b

k is V30() real ext-real set

n is V30() real ext-real Element of REAL

g2 is V30() real ext-real Element of REAL

{ b

k is V30() real ext-real Element of REAL

x0 is V30() real ext-real Element of REAL

f is V30() real ext-real Element of REAL

f + x0 is V30() real ext-real Element of REAL

].f,(f + x0).[ is V71() V72() V73() 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 V71() V72() V73() Element of K19(REAL)

s is V30() real ext-real Element of REAL

k is V30() real ext-real set

n is V30() real ext-real Element of REAL

g2 is V30() real ext-real Element of REAL

{ b

k is V30() real ext-real set

n is V30() real ext-real Element of REAL

g2 is V30() real ext-real Element of REAL

{ b

k is V30() real ext-real Element of REAL

x0 is V30() real ext-real Element of REAL

left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(-infty,x0) is set

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

rng f is V71() V72() V73() 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 V71() V72() V73() Element of K19(REAL)

(dom r) /\ (left_open_halfline x0) is V71() V72() V73() 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))

NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total T-Sequence-like complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,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))

k - 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 ) V6() total complex-valued ext-real-valued real-valued set

- 1 is V30() real ext-real non positive set

(- 1) (#) s is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set

k + (- s) is V1() V4( NAT ) V6() total complex-valued ext-real-valued real-valued set

n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

(k - s) . n is V30() real ext-real Element of REAL

k . n is V30() real ext-real Element of REAL

s . n is V30() real ext-real Element of REAL

(k . n) - (s . n) is V30() real ext-real Element of REAL

x0 - (s . n) is V30() real ext-real Element of REAL

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

1 / (n + 1) is V30() real ext-real non negative Element of REAL

x0 - (1 / (n + 1)) is V30() real ext-real Element of REAL

f . n is V30() real ext-real Element of REAL

k . 0 is V30() real ext-real Element of REAL

lim k is V30() real ext-real Element of REAL

lim s is V30() real ext-real Element of REAL

lim (k - s) is V30() real ext-real Element of REAL

x0 - 0 is V30() real ext-real Element of REAL

n is set

g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

f . g2 is V30() real ext-real Element of REAL

n is set

g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

f . g2 is V30() real ext-real Element of REAL

{ b

x0 is V30() real ext-real Element of REAL

right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(x0,+infty) is set

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

rng f is V71() V72() V73() 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 V71() V72() V73() Element of K19(REAL)

(dom r) /\ (right_open_halfline x0) is V71() V72() V73() 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))

NAT --> x0 is V1() V4( NAT ) V5( REAL ) V6() constant non empty total quasi_total T-Sequence-like complex-valued ext-real-valued real-valued convergent Element of K19(K20(NAT,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))

k + 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 non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

(k + s) . n is V30() real ext-real Element of REAL

k . n is V30() real ext-real Element of REAL

s . n is V30() real ext-real Element of REAL

(k . n) + (s . n) is V30() real ext-real Element of REAL

x0 + (s . n) is V30() real ext-real Element of REAL

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

1 / (n + 1) is V30() real ext-real non negative Element of REAL

x0 + (1 / (n + 1)) is V30() real ext-real Element of REAL

f . n is V30() real ext-real Element of REAL

k . 0 is V30() real ext-real Element of REAL

lim k is V30() real ext-real Element of REAL

lim s is V30() real ext-real Element of REAL

lim (k + s) is V30() real ext-real Element of REAL

x0 + 0 is V30() real ext-real Element of REAL

n is set

g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

f . g2 is V30() real ext-real Element of REAL

n is set

g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

f . g2 is V30() real ext-real Element of REAL

{ b

x0 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 V71() V72() V73() Element of K19(REAL)

left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(-infty,x0) is set

(dom f) /\ (left_open_halfline x0) is V71() V72() V73() 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 non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

1 / (k + 1) is V30() real ext-real non negative Element of REAL

x0 - (1 / (k + 1)) 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

(f . n) - r is V30() real ext-real Element of REAL

abs ((f . n) - r) is V30() real ext-real Element of REAL

g2 is V30() real ext-real Element of REAL

f . g2 is V30() real ext-real Element of REAL

(f . g2) - r is V30() real ext-real Element of REAL

abs ((f . g2) - r) 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))

rng k is V71() V72() V73() Element of K19(REAL)

lim k 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 epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() 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))

lim s is V30() real ext-real Element of REAL

rng s is V71() V72() V73() Element of K19(REAL)

left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(-infty,x0) is set

(dom f) /\ (left_open_halfline x0) is V71() V72() V73() 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 non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

s . g is V30() real ext-real Element of REAL

{ b

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

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

(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

x0 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 V71() V72() V73() 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 non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

1 / (s + 1) is V30() real ext-real non negative Element of REAL

x0 - (1 / (s + 1)) 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

n is V30() real ext-real Element of REAL

f . 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 V71() V72() V73() Element of K19(REAL)

left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(-infty,x0) is set

(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)

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

k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() 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))

lim r is V30() real ext-real Element of REAL

rng r is V71() V72() V73() Element of K19(REAL)

left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(-infty,x0) is set

(dom f) /\ (left_open_halfline x0) is V71() V72() V73() 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 non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

r . n is V30() real ext-real Element of REAL

{ b

f . (r . n) is V30() real ext-real Element of REAL

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) . n is V30() real ext-real Element of REAL

x0 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 V71() V72() V73() 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 non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

1 / (s + 1) is V30() real ext-real non negative Element of REAL

x0 - (1 / (s + 1)) 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

n is V30() real ext-real Element of REAL

f . 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 V71() V72() V73() Element of K19(REAL)

left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(-infty,x0) is set

(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)

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

k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() 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))

lim r is V30() real ext-real Element of REAL

rng r is V71() V72() V73() Element of K19(REAL)

left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(-infty,x0) is set

(dom f) /\ (left_open_halfline x0) is V71() V72() V73() 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 non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

r . n is V30() real ext-real Element of REAL

{ b

f . (r . n) is V30() real ext-real Element of REAL

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) . n is V30() real ext-real Element of REAL

x0 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 V71() V72() V73() Element of K19(REAL)

right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(x0,+infty) is set

(dom f) /\ (right_open_halfline x0) is V71() V72() V73() 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 non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

1 / (k + 1) is V30() real ext-real non negative Element of REAL

x0 + (1 / (k + 1)) 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

(f . n) - r is V30() real ext-real Element of REAL

abs ((f . n) - r) is V30() real ext-real Element of REAL

g2 is V30() real ext-real Element of REAL

f . g2 is V30() real ext-real Element of REAL

(f . g2) - r is V30() real ext-real Element of REAL

abs ((f . g2) - r) 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))

rng k is V71() V72() V73() Element of K19(REAL)

lim k 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 epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() 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))

lim s is V30() real ext-real Element of REAL

rng s is V71() V72() V73() Element of K19(REAL)

right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(x0,+infty) is set

(dom f) /\ (right_open_halfline x0) is V71() V72() V73() 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 non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

s . g is V30() real ext-real Element of REAL

{ b

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

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

(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

x0 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 V71() V72() V73() 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 non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

1 / (s + 1) is V30() real ext-real non negative Element of REAL

x0 + (1 / (s + 1)) 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

n is V30() real ext-real Element of REAL

f . 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 V71() V72() V73() Element of K19(REAL)

right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(x0,+infty) is set

(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)

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

k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() 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))

lim r is V30() real ext-real Element of REAL

rng r is V71() V72() V73() Element of K19(REAL)

right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(x0,+infty) is set

(dom f) /\ (right_open_halfline x0) is V71() V72() V73() 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 non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

r . n is V30() real ext-real Element of REAL

{ b

f . (r . n) is V30() real ext-real Element of REAL

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) . n is V30() real ext-real Element of REAL

x0 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 V71() V72() V73() 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 non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

1 / (s + 1) is V30() real ext-real non negative Element of REAL

x0 + (1 / (s + 1)) 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

n is V30() real ext-real Element of REAL

f . 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 V71() V72() V73() Element of K19(REAL)

right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(x0,+infty) is set

(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)

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

k is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() 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

right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(x0,+infty) is set

(dom f) /\ (right_open_halfline x0) is V71() V72() V73() 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))

lim r is V30() real ext-real Element of REAL

rng r is V71() V72() V73() 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))

x0 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 V71() V72() V73() 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 V71() V72() V73() Element of K19(REAL)

(dom f) /\ (dom r) is V71() V72() V73() 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))

lim s is V30() real ext-real Element of REAL

rng s is V71() V72() V73() Element of K19(REAL)

dom (f + r) is V71() V72() V73() Element of K19(REAL)

left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(-infty,x0) is set

(dom (f + r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)

(dom r) /\ (left_open_halfline x0) is V71() V72() V73() 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))

(dom f) /\ (left_open_halfline x0) is V71() V72() V73() 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))

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

lim s is V30() real ext-real Element of REAL

rng s is V71() V72() V73() Element of K19(REAL)

dom (f (#) r) is V71() V72() V73() Element of K19(REAL)

(dom (f (#) r)) /\ (left_open_halfline x0) is V71() V72() V73() 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

x0 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 V71() V72() V73() 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 V71() V72() V73() Element of K19(REAL)

(dom f) /\ (dom r) is V71() V72() V73() 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))

lim s is V30() real ext-real Element of REAL

rng s is V71() V72() V73() Element of K19(REAL)

dom (f + r) is V71() V72() V73() Element of K19(REAL)

left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(-infty,x0) is set

(dom (f + r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)

(dom r) /\ (left_open_halfline x0) is V71() V72() V73() 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))

(dom f) /\ (left_open_halfline x0) is V71() V72() V73() 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))

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

lim s is V30() real ext-real Element of REAL

rng s is V71() V72() V73() Element of K19(REAL)

dom (f (#) r) is V71() V72() V73() Element of K19(REAL)

(dom (f (#) r)) /\ (left_open_halfline x0) is V71() V72() V73() 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

x0 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 V71() V72() V73() 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 V71() V72() V73() Element of K19(REAL)

(dom f) /\ (dom r) is V71() V72() V73() 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))

lim s is V30() real ext-real Element of REAL

rng s is V71() V72() V73() Element of K19(REAL)

dom (f + r) is V71() V72() V73() Element of K19(REAL)

right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(x0,+infty) is set

(dom (f + r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)

(dom r) /\ (right_open_halfline x0) is V71() V72() V73() 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))

(dom f) /\ (right_open_halfline x0) is V71() V72() V73() 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))

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

lim s is V30() real ext-real Element of REAL

rng s is V71() V72() V73() Element of K19(REAL)

dom (f (#) r) is V71() V72() V73() Element of K19(REAL)

(dom (f (#) r)) /\ (right_open_halfline x0) is V71() V72() V73() 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

x0 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 V71() V72() V73() 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 V71() V72() V73() Element of K19(REAL)

(dom f) /\ (dom r) is V71() V72() V73() 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))

lim s is V30() real ext-real Element of REAL

rng s is V71() V72() V73() Element of K19(REAL)

dom (f + r) is V71() V72() V73() Element of K19(REAL)

right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(x0,+infty) is set

(dom (f + r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)

(dom r) /\ (right_open_halfline x0) is V71() V72() V73() 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))

(dom f) /\ (right_open_halfline x0) is V71() V72() V73() 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))

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

lim s is V30() real ext-real Element of REAL

rng s is V71() V72() V73() Element of K19(REAL)

dom (f (#) r) is V71() V72() V73() Element of K19(REAL)

(dom (f (#) r)) /\ (right_open_halfline x0) is V71() V72() V73() 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

x0 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 V71() V72() V73() Element of K19(REAL)

s is V30() real ext-real Element of REAL

x0 - s is V30() real ext-real Element of REAL

].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)

r | ].(x0 - s),x0.[ 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))

lim k is V30() real ext-real Element of REAL

rng k is V71() V72() V73() Element of K19(REAL)

left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(-infty,x0) is set

(dom (f + r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)

n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() 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 V71() V72() V73() Element of K19(REAL)

dom f is V71() V72() V73() Element of K19(REAL)

dom r is V71() V72() V73() Element of K19(REAL)

(dom f) /\ (dom r) is V71() V72() V73() 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

(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)

].(x0 - s),x0.[ /\ (dom r) is V71() V72() V73() Element of K19(REAL)

g2 is V30() real ext-real set

g2 - 1 is V30() real ext-real Element of REAL

g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

g + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() 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

{ b

{ b

n is V30() real ext-real Element of REAL

r . ((k ^\ n) . g) is V30() real ext-real Element of REAL

(r . ((k ^\ n) . g)) - 0 is V30() real ext-real Element of REAL

(r /* (k ^\ n)) . g 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

lim (k ^\ n) is V30() real ext-real Element of REAL

x0 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 V71() V72() V73() Element of K19(REAL)

dom r is V71() V72() V73() Element of K19(REAL)

s is V30() real ext-real Element of REAL

k is V30() real ext-real Element of REAL

x0 - s is V30() real ext-real Element of REAL

].(x0 - s),x0.[ is V71() V72() V73() Element of K19(REAL)

(dom r) /\ ].(x0 - s),x0.[ is V71() V72() V73() 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))

lim n is V30() real ext-real Element of REAL

rng n is V71() V72() V73() Element of K19(REAL)

left_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(-infty,x0) is set

(dom (f (#) r)) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)

g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

dom f is V71() V72() V73() Element of K19(REAL)

(dom f) /\ (dom r) is V71() V72() V73() Element of K19(REAL)

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 V71() V72() V73() Element of K19(REAL)

n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

n + g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

n . (n + g2) is V30() real ext-real Element of REAL

(n ^\ g2) . n is V30() real ext-real Element of REAL

{ b

{ b

g is V30() real ext-real Element of REAL

r . ((n ^\ g2) . n) 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)) . n is V30() real ext-real Element of REAL

(dom f) /\ (left_open_halfline x0) is V71() V72() V73() Element of K19(REAL)

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

(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

x0 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 V71() V72() V73() Element of K19(REAL)

s is V30() real ext-real Element of REAL

x0 + s is V30() real ext-real Element of REAL

].x0,(x0 + s).[ is V71() V72() V73() Element of K19(REAL)

r | ].x0,(x0 + 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))

lim k is V30() real ext-real Element of REAL

rng k is V71() V72() V73() Element of K19(REAL)

right_open_halfline x0 is V71() V72() V73() Element of K19(REAL)

K213(x0,+infty) is set

(dom (f + r)) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)

n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() 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 V71() V72() V73() Element of K19(REAL)

dom f is V71() V72() V73() Element of K19(REAL)

dom r is V71() V72() V73() Element of K19(REAL)

(dom f) /\ (dom r) is V71() V72() V73() 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

(dom f) /\ (right_open_halfline x0) is V71() V72() V73() Element of K19(REAL)

].x0,(x0 + s).[ /\ (dom r) is V71() V72() V73() Element of K19(REAL)

g2 is V30() real ext-real set

g2 - 1 is V30() real ext-real Element of REAL

g is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() Element of NAT

g + n is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V71() V72() V73() V74() V75() V76() V87() V88() 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

{ b

{ b

n is V30() real ext-real Element of REAL

r . ((k ^\ n) . g) is V30() real ext-real Element of REAL

(r . ((k ^\ n) . g)) - 0 is V30() real ext-real Element of REAL

(r /* (k ^\ n)) . g 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

lim (k ^\ n) is V30() real ext-real Element of REAL

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