:: LIMFUNC4 semantic presentation

NAT is V11() V15() V16() V17() V78() V79() V80() V81() V82() V83() V84() Element of K19(REAL)
REAL is V11() V49() V78() V79() V80() V84() set
K19(REAL) is set
NAT is V11() V15() V16() V17() V78() V79() V80() V81() V82() V83() V84() set
K19(NAT) is set
K20(NAT,REAL) is V33() V34() V35() set
K19(K20(NAT,REAL)) is set
K19(K19(REAL)) is set
COMPLEX is V11() V49() V78() V84() set
RAT is V11() V49() V78() V79() V80() V81() V84() set
INT is V11() V49() V78() V79() V80() V81() V82() V84() set
K20(REAL,REAL) is V33() V34() V35() set
K19(K20(REAL,REAL)) is set
0 is V11() V15() V16() V17() V19() V20() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() V84() Element of NAT
-infty is set
+infty is set
0 is V11() V15() V16() V17() V19() V20() V21() V78() V79() V80() V81() V82() V83() V84() set
x0 is V22() V23() ext-real Element of REAL
f1 is V22() V23() ext-real Element of REAL
f1 - x0 is V22() V23() ext-real Element of REAL
f1 + x0 is V22() V23() ext-real Element of REAL
f1 - 0 is V22() V23() ext-real Element of REAL
f1 + 0 is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
x0 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (x0 * f1) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f2 is V78() V79() V80() Element of K19(REAL)
f1 /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* f2) is V78() V79() V80() Element of K19(REAL)
g is set
s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(f1 /* f2) . s is V22() V23() ext-real Element of REAL
f2 . s is V22() V23() ext-real Element of REAL
f1 . (f2 . s) is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
x0 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (x0 * f1) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f2 is V78() V79() V80() Element of K19(REAL)
f1 /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* f2) is V78() V79() V80() Element of K19(REAL)
g is set
(dom (x0 * f1)) /\ g is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ g is V78() V79() V80() Element of K19(REAL)
s is set
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(f1 /* f2) . k is V22() V23() ext-real Element of REAL
f2 . k is V22() V23() ext-real Element of REAL
f1 . (f2 . k) is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
x0 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (x0 * f1) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f2 is V78() V79() V80() Element of K19(REAL)
f1 /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* f2) is V78() V79() V80() Element of K19(REAL)
g is set
(dom (x0 * f1)) \ g is V78() V79() V80() Element of K19(REAL)
(dom f1) \ g is V78() V79() V80() Element of K19(REAL)
s is set
s is set
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(f1 /* f2) . k is V22() V23() ext-real Element of REAL
f2 . k is V22() V23() ext-real Element of REAL
f1 . (f2 . k) is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f2 is V78() V79() V80() Element of K19(REAL)
dom x0 is V78() V79() V80() Element of K19(REAL)
x0 /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* f2) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
f1 /* (x0 /* f2) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 * x0) /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f2 is V78() V79() V80() Element of K19(REAL)
dom x0 is V78() V79() V80() Element of K19(REAL)
x0 /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* f2) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
f1 /* (x0 /* f2) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 * x0) /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f2 is V78() V79() V80() Element of K19(REAL)
dom x0 is V78() V79() V80() Element of K19(REAL)
x0 /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* f2) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
f1 /* (x0 /* f2) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 * x0) /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f2 is V78() V79() V80() Element of K19(REAL)
dom x0 is V78() V79() V80() Element of K19(REAL)
x0 /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* f2) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
f1 /* (x0 /* f2) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 * x0) /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f2 is V78() V79() V80() Element of K19(REAL)
dom x0 is V78() V79() V80() Element of K19(REAL)
x0 /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* f2) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
f1 /* (x0 /* f2) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 * x0) /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f2 is V78() V79() V80() Element of K19(REAL)
dom x0 is V78() V79() V80() Element of K19(REAL)
x0 /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* f2) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
f1 /* (x0 /* f2) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 * x0) /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f2 is V78() V79() V80() Element of K19(REAL)
dom x0 is V78() V79() V80() Element of K19(REAL)
x0 /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* f2) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
f1 /* (x0 /* f2) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 * x0) /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f2 is V78() V79() V80() Element of K19(REAL)
dom x0 is V78() V79() V80() Element of K19(REAL)
x0 /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* f2) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
f1 /* (x0 /* f2) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 * x0) /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
left_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(-infty,x0) is set
(dom (f2 * f1)) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
left_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(-infty,x0) is set
(dom (f2 * f1)) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
left_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(-infty,x0) is set
(dom (f2 * f1)) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
left_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(-infty,x0) is set
(dom (f2 * f1)) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
right_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(x0,+infty) is set
(dom (f2 * f1)) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
right_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(x0,+infty) is set
(dom (f2 * f1)) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
right_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(x0,+infty) is set
(dom (f2 * f1)) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
right_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(x0,+infty) is set
(dom (f2 * f1)) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_left (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
left_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(-infty,x0) is set
(dom (f2 * f1)) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not lim_left (f1,x0) <= b₁ } is set
left_open_halfline (lim_left (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177(-infty,(lim_left (f1,x0))) is set
(dom f2) /\ (left_open_halfline (lim_left (f1,x0))) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_left (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
left_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(-infty,x0) is set
(dom (f2 * f1)) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not lim_left (f1,x0) <= b₁ } is set
left_open_halfline (lim_left (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177(-infty,(lim_left (f1,x0))) is set
(dom f2) /\ (left_open_halfline (lim_left (f1,x0))) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_left (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
left_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(-infty,x0) is set
(dom (f2 * f1)) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= lim_left (f1,x0) } is set
right_open_halfline (lim_left (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177((lim_left (f1,x0)),+infty) is set
(dom f2) /\ (right_open_halfline (lim_left (f1,x0))) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_left (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
left_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(-infty,x0) is set
(dom (f2 * f1)) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= lim_left (f1,x0) } is set
right_open_halfline (lim_left (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177((lim_left (f1,x0)),+infty) is set
(dom f2) /\ (right_open_halfline (lim_left (f1,x0))) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_right (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
right_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(x0,+infty) is set
(dom (f2 * f1)) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 & not x0 + g <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= lim_right (f1,x0) } is set
right_open_halfline (lim_right (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177((lim_right (f1,x0)),+infty) is set
(dom f2) /\ (right_open_halfline (lim_right (f1,x0))) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_right (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
right_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(x0,+infty) is set
(dom (f2 * f1)) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 & not x0 + g <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= lim_right (f1,x0) } is set
right_open_halfline (lim_right (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177((lim_right (f1,x0)),+infty) is set
(dom f2) /\ (right_open_halfline (lim_right (f1,x0))) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_right (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
right_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(x0,+infty) is set
(dom (f2 * f1)) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 & not x0 + g <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not lim_right (f1,x0) <= b₁ } is set
left_open_halfline (lim_right (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177(-infty,(lim_right (f1,x0))) is set
(dom f2) /\ (left_open_halfline (lim_right (f1,x0))) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_right (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
right_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(x0,+infty) is set
(dom (f2 * f1)) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 & not x0 + g <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not lim_right (f1,x0) <= b₁ } is set
left_open_halfline (lim_right (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177(-infty,(lim_right (f1,x0))) is set
(dom f2) /\ (left_open_halfline (lim_right (f1,x0))) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in+infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V22() V23() ext-real Element of REAL
right_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(f2,+infty) is set
(dom x0) /\ (right_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng g is V78() V79() V80() Element of K19(REAL)
s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
x0 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* g) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
g ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,g)
rng (g ^\ s) is V78() V79() V80() Element of K19(REAL)
x0 /* (g ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* (g ^\ s)) is V78() V79() V80() Element of K19(REAL)
left_open_halfline (lim_in+infty x0) is V78() V79() V80() Element of K19(REAL)
K177(-infty,(lim_in+infty x0)) is set
(dom f1) /\ (left_open_halfline (lim_in+infty x0)) is V78() V79() V80() Element of K19(REAL)
q is set
x is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (g ^\ s)) . x is V22() V23() ext-real Element of REAL
(g ^\ s) . x is V22() V23() ext-real Element of REAL
x0 . ((g ^\ s) . x) is V22() V23() ext-real Element of REAL
x + s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
g . (x + s) is V22() V23() ext-real Element of REAL
x0 . (g . (x + s)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= f2 } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not lim_in+infty x0 <= b₁ } is set
(x0 /* g) . (x + s) is V22() V23() ext-real Element of REAL
lim (x0 /* (g ^\ s)) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (g ^\ s)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* g)
f1 /* ((x0 /* g) ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* g)) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* g))
(f1 * x0) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* g)
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in+infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V22() V23() ext-real Element of REAL
right_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(f2,+infty) is set
(dom x0) /\ (right_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng g is V78() V79() V80() Element of K19(REAL)
s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
x0 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* g) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
g ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,g)
rng (g ^\ s) is V78() V79() V80() Element of K19(REAL)
x0 /* (g ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* (g ^\ s)) is V78() V79() V80() Element of K19(REAL)
left_open_halfline (lim_in+infty x0) is V78() V79() V80() Element of K19(REAL)
K177(-infty,(lim_in+infty x0)) is set
(dom f1) /\ (left_open_halfline (lim_in+infty x0)) is V78() V79() V80() Element of K19(REAL)
q is set
x is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (g ^\ s)) . x is V22() V23() ext-real Element of REAL
(g ^\ s) . x is V22() V23() ext-real Element of REAL
x0 . ((g ^\ s) . x) is V22() V23() ext-real Element of REAL
x + s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
g . (x + s) is V22() V23() ext-real Element of REAL
x0 . (g . (x + s)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= f2 } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not lim_in+infty x0 <= b₁ } is set
(x0 /* g) . (x + s) is V22() V23() ext-real Element of REAL
lim (x0 /* (g ^\ s)) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (g ^\ s)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* g)
f1 /* ((x0 /* g) ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* g)) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* g))
(f1 * x0) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* g)
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in+infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V22() V23() ext-real Element of REAL
right_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(f2,+infty) is set
(dom x0) /\ (right_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng g is V78() V79() V80() Element of K19(REAL)
s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
x0 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* g) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
g ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,g)
rng (g ^\ s) is V78() V79() V80() Element of K19(REAL)
x0 /* (g ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* (g ^\ s)) is V78() V79() V80() Element of K19(REAL)
right_open_halfline (lim_in+infty x0) is V78() V79() V80() Element of K19(REAL)
K177((lim_in+infty x0),+infty) is set
(dom f1) /\ (right_open_halfline (lim_in+infty x0)) is V78() V79() V80() Element of K19(REAL)
q is set
x is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (g ^\ s)) . x is V22() V23() ext-real Element of REAL
(g ^\ s) . x is V22() V23() ext-real Element of REAL
x0 . ((g ^\ s) . x) is V22() V23() ext-real Element of REAL
x + s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
g . (x + s) is V22() V23() ext-real Element of REAL
x0 . (g . (x + s)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= f2 } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= lim_in+infty x0 } is set
(x0 /* g) . (x + s) is V22() V23() ext-real Element of REAL
lim (x0 /* (g ^\ s)) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (g ^\ s)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* g)
f1 /* ((x0 /* g) ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* g)) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* g))
(f1 * x0) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* g)
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in+infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V22() V23() ext-real Element of REAL
right_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(f2,+infty) is set
(dom x0) /\ (right_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng g is V78() V79() V80() Element of K19(REAL)
s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
x0 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* g) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
g ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,g)
rng (g ^\ s) is V78() V79() V80() Element of K19(REAL)
x0 /* (g ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* (g ^\ s)) is V78() V79() V80() Element of K19(REAL)
right_open_halfline (lim_in+infty x0) is V78() V79() V80() Element of K19(REAL)
K177((lim_in+infty x0),+infty) is set
(dom f1) /\ (right_open_halfline (lim_in+infty x0)) is V78() V79() V80() Element of K19(REAL)
q is set
x is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (g ^\ s)) . x is V22() V23() ext-real Element of REAL
(g ^\ s) . x is V22() V23() ext-real Element of REAL
x0 . ((g ^\ s) . x) is V22() V23() ext-real Element of REAL
x + s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
g . (x + s) is V22() V23() ext-real Element of REAL
x0 . (g . (x + s)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= f2 } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= lim_in+infty x0 } is set
(x0 /* g) . (x + s) is V22() V23() ext-real Element of REAL
lim (x0 /* (g ^\ s)) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (g ^\ s)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* g)
f1 /* ((x0 /* g) ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* g)) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* g))
(f1 * x0) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* g)
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in-infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V22() V23() ext-real Element of REAL
left_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(-infty,f2) is set
(dom x0) /\ (left_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng g is V78() V79() V80() Element of K19(REAL)
s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
x0 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* g) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
g ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,g)
rng (g ^\ s) is V78() V79() V80() Element of K19(REAL)
x0 /* (g ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* (g ^\ s)) is V78() V79() V80() Element of K19(REAL)
left_open_halfline (lim_in-infty x0) is V78() V79() V80() Element of K19(REAL)
K177(-infty,(lim_in-infty x0)) is set
(dom f1) /\ (left_open_halfline (lim_in-infty x0)) is V78() V79() V80() Element of K19(REAL)
q is set
x is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (g ^\ s)) . x is V22() V23() ext-real Element of REAL
(g ^\ s) . x is V22() V23() ext-real Element of REAL
x0 . ((g ^\ s) . x) is V22() V23() ext-real Element of REAL
x + s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
g . (x + s) is V22() V23() ext-real Element of REAL
x0 . (g . (x + s)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not f2 <= b₁ } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not lim_in-infty x0 <= b₁ } is set
(x0 /* g) . (x + s) is V22() V23() ext-real Element of REAL
lim (x0 /* (g ^\ s)) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (g ^\ s)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* g)
f1 /* ((x0 /* g) ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* g)) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* g))
(f1 * x0) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* g)
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in-infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V22() V23() ext-real Element of REAL
left_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(-infty,f2) is set
(dom x0) /\ (left_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng g is V78() V79() V80() Element of K19(REAL)
s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
x0 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* g) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
g ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,g)
rng (g ^\ s) is V78() V79() V80() Element of K19(REAL)
x0 /* (g ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* (g ^\ s)) is V78() V79() V80() Element of K19(REAL)
left_open_halfline (lim_in-infty x0) is V78() V79() V80() Element of K19(REAL)
K177(-infty,(lim_in-infty x0)) is set
(dom f1) /\ (left_open_halfline (lim_in-infty x0)) is V78() V79() V80() Element of K19(REAL)
q is set
x is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (g ^\ s)) . x is V22() V23() ext-real Element of REAL
(g ^\ s) . x is V22() V23() ext-real Element of REAL
x0 . ((g ^\ s) . x) is V22() V23() ext-real Element of REAL
x + s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
g . (x + s) is V22() V23() ext-real Element of REAL
x0 . (g . (x + s)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not f2 <= b₁ } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not lim_in-infty x0 <= b₁ } is set
(x0 /* g) . (x + s) is V22() V23() ext-real Element of REAL
lim (x0 /* (g ^\ s)) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (g ^\ s)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* g)
f1 /* ((x0 /* g) ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* g)) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* g))
(f1 * x0) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* g)
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in-infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V22() V23() ext-real Element of REAL
left_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(-infty,f2) is set
(dom x0) /\ (left_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng g is V78() V79() V80() Element of K19(REAL)
s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
x0 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* g) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
g ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,g)
rng (g ^\ s) is V78() V79() V80() Element of K19(REAL)
x0 /* (g ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* (g ^\ s)) is V78() V79() V80() Element of K19(REAL)
right_open_halfline (lim_in-infty x0) is V78() V79() V80() Element of K19(REAL)
K177((lim_in-infty x0),+infty) is set
(dom f1) /\ (right_open_halfline (lim_in-infty x0)) is V78() V79() V80() Element of K19(REAL)
q is set
x is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (g ^\ s)) . x is V22() V23() ext-real Element of REAL
(g ^\ s) . x is V22() V23() ext-real Element of REAL
x0 . ((g ^\ s) . x) is V22() V23() ext-real Element of REAL
x + s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
g . (x + s) is V22() V23() ext-real Element of REAL
x0 . (g . (x + s)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not f2 <= b₁ } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= lim_in-infty x0 } is set
(x0 /* g) . (x + s) is V22() V23() ext-real Element of REAL
lim (x0 /* (g ^\ s)) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (g ^\ s)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* g)
f1 /* ((x0 /* g) ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* g)) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* g))
(f1 * x0) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* g)
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in-infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V22() V23() ext-real Element of REAL
left_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(-infty,f2) is set
(dom x0) /\ (left_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng g is V78() V79() V80() Element of K19(REAL)
s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
x0 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* g) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
g ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,g)
rng (g ^\ s) is V78() V79() V80() Element of K19(REAL)
x0 /* (g ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* (g ^\ s)) is V78() V79() V80() Element of K19(REAL)
right_open_halfline (lim_in-infty x0) is V78() V79() V80() Element of K19(REAL)
K177((lim_in-infty x0),+infty) is set
(dom f1) /\ (right_open_halfline (lim_in-infty x0)) is V78() V79() V80() Element of K19(REAL)
q is set
x is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (g ^\ s)) . x is V22() V23() ext-real Element of REAL
(g ^\ s) . x is V22() V23() ext-real Element of REAL
x0 . ((g ^\ s) . x) is V22() V23() ext-real Element of REAL
x + s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
g . (x + s) is V22() V23() ext-real Element of REAL
x0 . (g . (x + s)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not f2 <= b₁ } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= lim_in-infty x0 } is set
(x0 /* g) . (x + s) is V22() V23() ext-real Element of REAL
lim (x0 /* (g ^\ s)) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (g ^\ s)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* g)
f1 /* ((x0 /* g) ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* g)) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* g))
(f1 * x0) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* g)
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
{x0} is V11() V78() V79() V80() set
(dom (f2 * f1)) \ {x0} is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) \ {x0} is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
{x0} is V11() V78() V79() V80() set
(dom (f2 * f1)) \ {x0} is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) \ {x0} is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
{x0} is V11() V78() V79() V80() set
(dom (f2 * f1)) \ {x0} is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) \ {x0} is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
{x0} is V11() V78() V79() V80() set
(dom (f2 * f1)) \ {x0} is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) \ {x0} is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
{x0} is V11() V78() V79() V80() set
(dom (f2 * f1)) \ {x0} is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) \ {x0} is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 + g <= b₁ ) } is set
].(x0 - g),(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),(x0 + g).[ \ {x0} is V78() V79() V80() Element of K19(REAL)
{(lim (f1,x0))} is V11() V78() V79() V80() set
(dom f2) \ {(lim (f1,x0))} is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
{x0} is V11() V78() V79() V80() set
(dom (f2 * f1)) \ {x0} is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) \ {x0} is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 + g <= b₁ ) } is set
].(x0 - g),(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),(x0 + g).[ \ {x0} is V78() V79() V80() Element of K19(REAL)
{(lim (f1,x0))} is V11() V78() V79() V80() set
(dom f2) \ {(lim (f1,x0))} is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
{x0} is V11() V78() V79() V80() set
(dom (f2 * f1)) \ {x0} is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) \ {x0} is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 + g <= b₁ ) } is set
].(x0 - g),(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),(x0 + g).[ \ {x0} is V78() V79() V80() Element of K19(REAL)
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= lim (f1,x0) } is set
right_open_halfline (lim (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177((lim (f1,x0)),+infty) is set
(dom f2) /\ (right_open_halfline (lim (f1,x0))) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
{x0} is V11() V78() V79() V80() set
(dom (f2 * f1)) \ {x0} is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) \ {x0} is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 + g <= b₁ ) } is set
].(x0 - g),(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),(x0 + g).[ \ {x0} is V78() V79() V80() Element of K19(REAL)
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= lim (f1,x0) } is set
right_open_halfline (lim (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177((lim (f1,x0)),+infty) is set
(dom f2) /\ (right_open_halfline (lim (f1,x0))) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_right (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
right_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(x0,+infty) is set
(dom (f2 * f1)) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 & not x0 + g <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{(lim_right (f1,x0))} is V11() V78() V79() V80() set
(dom f2) \ {(lim_right (f1,x0))} is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_right (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
right_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(x0,+infty) is set
(dom (f2 * f1)) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 & not x0 + g <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{(lim_right (f1,x0))} is V11() V78() V79() V80() set
(dom f2) \ {(lim_right (f1,x0))} is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in+infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V22() V23() ext-real Element of REAL
right_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(f2,+infty) is set
(dom x0) /\ (right_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng g is V78() V79() V80() Element of K19(REAL)
s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
x0 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* g) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
g ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,g)
rng (g ^\ s) is V78() V79() V80() Element of K19(REAL)
x0 /* (g ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* (g ^\ s)) is V78() V79() V80() Element of K19(REAL)
{(lim_in+infty x0)} is V11() V78() V79() V80() set
(dom f1) \ {(lim_in+infty x0)} is V78() V79() V80() Element of K19(REAL)
q is set
x is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (g ^\ s)) . x is V22() V23() ext-real Element of REAL
(g ^\ s) . x is V22() V23() ext-real Element of REAL
x0 . ((g ^\ s) . x) is V22() V23() ext-real Element of REAL
x + s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
g . (x + s) is V22() V23() ext-real Element of REAL
x0 . (g . (x + s)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= f2 } is set
(x0 /* g) . (x + s) is V22() V23() ext-real Element of REAL
lim (x0 /* (g ^\ s)) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (g ^\ s)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* g)
f1 /* ((x0 /* g) ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* g)) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* g))
(f1 * x0) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* g)
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in+infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V22() V23() ext-real Element of REAL
right_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(f2,+infty) is set
(dom x0) /\ (right_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng g is V78() V79() V80() Element of K19(REAL)
s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
x0 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* g) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
g ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,g)
rng (g ^\ s) is V78() V79() V80() Element of K19(REAL)
x0 /* (g ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* (g ^\ s)) is V78() V79() V80() Element of K19(REAL)
{(lim_in+infty x0)} is V11() V78() V79() V80() set
(dom f1) \ {(lim_in+infty x0)} is V78() V79() V80() Element of K19(REAL)
q is set
x is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (g ^\ s)) . x is V22() V23() ext-real Element of REAL
(g ^\ s) . x is V22() V23() ext-real Element of REAL
x0 . ((g ^\ s) . x) is V22() V23() ext-real Element of REAL
x + s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
g . (x + s) is V22() V23() ext-real Element of REAL
x0 . (g . (x + s)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= f2 } is set
(x0 /* g) . (x + s) is V22() V23() ext-real Element of REAL
lim (x0 /* (g ^\ s)) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (g ^\ s)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* g)
f1 /* ((x0 /* g) ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* g)) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* g))
(f1 * x0) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* g)
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in-infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V22() V23() ext-real Element of REAL
left_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(-infty,f2) is set
(dom x0) /\ (left_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng g is V78() V79() V80() Element of K19(REAL)
s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
x0 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* g) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
g ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,g)
rng (g ^\ s) is V78() V79() V80() Element of K19(REAL)
x0 /* (g ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* (g ^\ s)) is V78() V79() V80() Element of K19(REAL)
{(lim_in-infty x0)} is V11() V78() V79() V80() set
(dom f1) \ {(lim_in-infty x0)} is V78() V79() V80() Element of K19(REAL)
q is set
x is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (g ^\ s)) . x is V22() V23() ext-real Element of REAL
(g ^\ s) . x is V22() V23() ext-real Element of REAL
x0 . ((g ^\ s) . x) is V22() V23() ext-real Element of REAL
x + s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
g . (x + s) is V22() V23() ext-real Element of REAL
x0 . (g . (x + s)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not f2 <= b₁ } is set
(x0 /* g) . (x + s) is V22() V23() ext-real Element of REAL
lim (x0 /* (g ^\ s)) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (g ^\ s)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* g)
f1 /* ((x0 /* g) ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* g)) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* g))
(f1 * x0) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* g)
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in-infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
f2 is V22() V23() ext-real Element of REAL
left_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(-infty,f2) is set
(dom x0) /\ (left_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng g is V78() V79() V80() Element of K19(REAL)
s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
x0 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* g) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
g ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,g)
rng (g ^\ s) is V78() V79() V80() Element of K19(REAL)
x0 /* (g ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* (g ^\ s)) is V78() V79() V80() Element of K19(REAL)
{(lim_in-infty x0)} is V11() V78() V79() V80() set
(dom f1) \ {(lim_in-infty x0)} is V78() V79() V80() Element of K19(REAL)
q is set
x is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (g ^\ s)) . x is V22() V23() ext-real Element of REAL
(g ^\ s) . x is V22() V23() ext-real Element of REAL
x0 . ((g ^\ s) . x) is V22() V23() ext-real Element of REAL
x + s is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
g . (x + s) is V22() V23() ext-real Element of REAL
x0 . (g . (x + s)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not f2 <= b₁ } is set
(x0 /* g) . (x + s) is V22() V23() ext-real Element of REAL
lim (x0 /* (g ^\ s)) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (g ^\ s)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* g)
f1 /* ((x0 /* g) ^\ s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* g)) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* g))
(f1 * x0) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* g) ^\ s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* g)
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
{x0} is V11() V78() V79() V80() set
(dom (f2 * f1)) \ {x0} is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) \ {x0} is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 + g <= b₁ ) } is set
].(x0 - g),(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),(x0 + g).[ \ {x0} is V78() V79() V80() Element of K19(REAL)
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not lim (f1,x0) <= b₁ } is set
left_open_halfline (lim (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177(-infty,(lim (f1,x0))) is set
(dom f2) /\ (left_open_halfline (lim (f1,x0))) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
{x0} is V11() V78() V79() V80() set
(dom (f2 * f1)) \ {x0} is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) \ {x0} is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 + g <= b₁ ) } is set
].(x0 - g),(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),(x0 + g).[ \ {x0} is V78() V79() V80() Element of K19(REAL)
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not lim (f1,x0) <= b₁ } is set
left_open_halfline (lim (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177(-infty,(lim (f1,x0))) is set
(dom f2) /\ (left_open_halfline (lim (f1,x0))) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_left (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
left_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(-infty,x0) is set
(dom (f2 * f1)) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{(lim_left (f1,x0))} is V11() V78() V79() V80() set
(dom f2) \ {(lim_left (f1,x0))} is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_left (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
left_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(-infty,x0) is set
(dom (f2 * f1)) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{(lim_left (f1,x0))} is V11() V78() V79() V80() set
(dom f2) \ {(lim_left (f1,x0))} is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
lim_in+infty (f1 * x0) is V22() V23() ext-real Element of REAL
lim_in+infty f1 is V22() V23() ext-real Element of REAL
f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f2 is V78() V79() V80() Element of K19(REAL)
dom x0 is V78() V79() V80() Element of K19(REAL)
x0 /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* f2) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
f1 /* (x0 /* f2) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (f1 /* (x0 /* f2)) is V22() V23() ext-real Element of REAL
(f1 * x0) /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim ((f1 * x0) /* f2) is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
lim_in+infty (f1 * x0) is V22() V23() ext-real Element of REAL
lim_in-infty f1 is V22() V23() ext-real Element of REAL
f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f2 is V78() V79() V80() Element of K19(REAL)
dom x0 is V78() V79() V80() Element of K19(REAL)
x0 /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* f2) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
f1 /* (x0 /* f2) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (f1 /* (x0 /* f2)) is V22() V23() ext-real Element of REAL
(f1 * x0) /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim ((f1 * x0) /* f2) is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
lim_in-infty (f1 * x0) is V22() V23() ext-real Element of REAL
lim_in+infty f1 is V22() V23() ext-real Element of REAL
f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f2 is V78() V79() V80() Element of K19(REAL)
dom x0 is V78() V79() V80() Element of K19(REAL)
x0 /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* f2) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
f1 /* (x0 /* f2) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (f1 /* (x0 /* f2)) is V22() V23() ext-real Element of REAL
(f1 * x0) /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim ((f1 * x0) /* f2) is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
lim_in-infty (f1 * x0) is V22() V23() ext-real Element of REAL
lim_in-infty f1 is V22() V23() ext-real Element of REAL
f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f2 is V78() V79() V80() Element of K19(REAL)
dom x0 is V78() V79() V80() Element of K19(REAL)
x0 /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* f2) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
f1 /* (x0 /* f2) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (f1 /* (x0 /* f2)) is V22() V23() ext-real Element of REAL
(f1 * x0) /* f2 is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim ((f1 * x0) /* f2) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
lim_left ((f2 * f1),x0) is V22() V23() ext-real Element of REAL
lim_in+infty f2 is V22() V23() ext-real Element of REAL
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
left_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(-infty,x0) is set
(dom (f2 * f1)) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (f2 /* (f1 /* g)) is V22() V23() ext-real Element of REAL
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim ((f2 * f1) /* g) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
lim_left ((f2 * f1),x0) is V22() V23() ext-real Element of REAL
lim_in-infty f2 is V22() V23() ext-real Element of REAL
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
left_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(-infty,x0) is set
(dom (f2 * f1)) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (f2 /* (f1 /* g)) is V22() V23() ext-real Element of REAL
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim ((f2 * f1) /* g) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
lim_right ((f2 * f1),x0) is V22() V23() ext-real Element of REAL
lim_in+infty f2 is V22() V23() ext-real Element of REAL
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
right_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(x0,+infty) is set
(dom (f2 * f1)) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (f2 /* (f1 /* g)) is V22() V23() ext-real Element of REAL
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim ((f2 * f1) /* g) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
lim_right ((f2 * f1),x0) is V22() V23() ext-real Element of REAL
lim_in-infty f2 is V22() V23() ext-real Element of REAL
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
right_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(x0,+infty) is set
(dom (f2 * f1)) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (f2 /* (f1 /* g)) is V22() V23() ext-real Element of REAL
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim ((f2 * f1) /* g) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_left (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
lim_left ((f2 * f1),x0) is V22() V23() ext-real Element of REAL
lim_left (f2,(lim_left (f1,x0))) is V22() V23() ext-real Element of REAL
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
left_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(-infty,x0) is set
(dom (f2 * f1)) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not lim_left (f1,x0) <= b₁ } is set
left_open_halfline (lim_left (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177(-infty,(lim_left (f1,x0))) is set
dom f2 is V78() V79() V80() Element of K19(REAL)
(dom f2) /\ (left_open_halfline (lim_left (f1,x0))) is V78() V79() V80() Element of K19(REAL)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
lim (f2 /* ((f1 /* s) ^\ k)) is V22() V23() ext-real Element of REAL
lim ((f2 * f1) /* s) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_right (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
lim_right ((f2 * f1),x0) is V22() V23() ext-real Element of REAL
lim_right (f2,(lim_right (f1,x0))) is V22() V23() ext-real Element of REAL
g is V22() V23() ext-real Element of REAL
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
right_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(x0,+infty) is set
(dom (f2 * f1)) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 & not x0 + g <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= lim_right (f1,x0) } is set
right_open_halfline (lim_right (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177((lim_right (f1,x0)),+infty) is set
dom f2 is V78() V79() V80() Element of K19(REAL)
(dom f2) /\ (right_open_halfline (lim_right (f1,x0))) is V78() V79() V80() Element of K19(REAL)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
lim (f2 /* ((f1 /* s) ^\ k)) is V22() V23() ext-real Element of REAL
lim ((f2 * f1) /* s) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_left (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
lim_left ((f2 * f1),x0) is V22() V23() ext-real Element of REAL
lim_right (f2,(lim_left (f1,x0))) is V22() V23() ext-real Element of REAL
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
left_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(-infty,x0) is set
(dom (f2 * f1)) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= lim_left (f1,x0) } is set
right_open_halfline (lim_left (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177((lim_left (f1,x0)),+infty) is set
dom f2 is V78() V79() V80() Element of K19(REAL)
(dom f2) /\ (right_open_halfline (lim_left (f1,x0))) is V78() V79() V80() Element of K19(REAL)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
lim (f2 /* ((f1 /* s) ^\ k)) is V22() V23() ext-real Element of REAL
lim ((f2 * f1) /* s) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_right (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
lim_right ((f2 * f1),x0) is V22() V23() ext-real Element of REAL
lim_left (f2,(lim_right (f1,x0))) is V22() V23() ext-real Element of REAL
g is V22() V23() ext-real Element of REAL
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
right_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(x0,+infty) is set
(dom (f2 * f1)) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 & not x0 + g <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not lim_right (f1,x0) <= b₁ } is set
left_open_halfline (lim_right (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177(-infty,(lim_right (f1,x0))) is set
dom f2 is V78() V79() V80() Element of K19(REAL)
(dom f2) /\ (left_open_halfline (lim_right (f1,x0))) is V78() V79() V80() Element of K19(REAL)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
lim (f2 /* ((f1 /* s) ^\ k)) is V22() V23() ext-real Element of REAL
lim ((f2 * f1) /* s) is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in+infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
lim_in+infty (f1 * x0) is V22() V23() ext-real Element of REAL
lim_left (f1,(lim_in+infty x0)) is V22() V23() ext-real Element of REAL
f2 is V22() V23() ext-real Element of REAL
right_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(f2,+infty) is set
(dom x0) /\ (right_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng s is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,s)
rng (s ^\ k) is V78() V79() V80() Element of K19(REAL)
x0 /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (x0 /* (s ^\ k)) is V22() V23() ext-real Element of REAL
x0 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* s) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
rng (x0 /* (s ^\ k)) is V78() V79() V80() Element of K19(REAL)
left_open_halfline (lim_in+infty x0) is V78() V79() V80() Element of K19(REAL)
K177(-infty,(lim_in+infty x0)) is set
(dom f1) /\ (left_open_halfline (lim_in+infty x0)) is V78() V79() V80() Element of K19(REAL)
x is set
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (s ^\ k)) . n is V22() V23() ext-real Element of REAL
(s ^\ k) . n is V22() V23() ext-real Element of REAL
x0 . ((s ^\ k) . n) is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
x0 . (s . (n + k)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= f2 } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not lim_in+infty x0 <= b₁ } is set
(x0 /* s) . (n + k) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (s ^\ k)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* s)
f1 /* ((x0 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* s))
(f1 * x0) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* s)
lim (f1 /* (x0 /* (s ^\ k))) is V22() V23() ext-real Element of REAL
lim ((f1 * x0) /* s) is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in+infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
lim_in+infty (f1 * x0) is V22() V23() ext-real Element of REAL
lim_right (f1,(lim_in+infty x0)) is V22() V23() ext-real Element of REAL
f2 is V22() V23() ext-real Element of REAL
right_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(f2,+infty) is set
(dom x0) /\ (right_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng s is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,s)
rng (s ^\ k) is V78() V79() V80() Element of K19(REAL)
x0 /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (x0 /* (s ^\ k)) is V22() V23() ext-real Element of REAL
x0 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* s) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
rng (x0 /* (s ^\ k)) is V78() V79() V80() Element of K19(REAL)
right_open_halfline (lim_in+infty x0) is V78() V79() V80() Element of K19(REAL)
K177((lim_in+infty x0),+infty) is set
(dom f1) /\ (right_open_halfline (lim_in+infty x0)) is V78() V79() V80() Element of K19(REAL)
x is set
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (s ^\ k)) . n is V22() V23() ext-real Element of REAL
(s ^\ k) . n is V22() V23() ext-real Element of REAL
x0 . ((s ^\ k) . n) is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
x0 . (s . (n + k)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= f2 } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= lim_in+infty x0 } is set
(x0 /* s) . (n + k) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (s ^\ k)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* s)
f1 /* ((x0 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* s))
(f1 * x0) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* s)
lim (f1 /* (x0 /* (s ^\ k))) is V22() V23() ext-real Element of REAL
lim ((f1 * x0) /* s) is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in-infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
lim_in-infty (f1 * x0) is V22() V23() ext-real Element of REAL
lim_left (f1,(lim_in-infty x0)) is V22() V23() ext-real Element of REAL
f2 is V22() V23() ext-real Element of REAL
left_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(-infty,f2) is set
(dom x0) /\ (left_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng s is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,s)
rng (s ^\ k) is V78() V79() V80() Element of K19(REAL)
x0 /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (x0 /* (s ^\ k)) is V22() V23() ext-real Element of REAL
x0 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* s) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
rng (x0 /* (s ^\ k)) is V78() V79() V80() Element of K19(REAL)
left_open_halfline (lim_in-infty x0) is V78() V79() V80() Element of K19(REAL)
K177(-infty,(lim_in-infty x0)) is set
(dom f1) /\ (left_open_halfline (lim_in-infty x0)) is V78() V79() V80() Element of K19(REAL)
x is set
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (s ^\ k)) . n is V22() V23() ext-real Element of REAL
(s ^\ k) . n is V22() V23() ext-real Element of REAL
x0 . ((s ^\ k) . n) is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
x0 . (s . (n + k)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not f2 <= b₁ } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not lim_in-infty x0 <= b₁ } is set
(x0 /* s) . (n + k) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (s ^\ k)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* s)
f1 /* ((x0 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* s))
(f1 * x0) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* s)
lim (f1 /* (x0 /* (s ^\ k))) is V22() V23() ext-real Element of REAL
lim ((f1 * x0) /* s) is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in-infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
lim_in-infty (f1 * x0) is V22() V23() ext-real Element of REAL
lim_right (f1,(lim_in-infty x0)) is V22() V23() ext-real Element of REAL
f2 is V22() V23() ext-real Element of REAL
left_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(-infty,f2) is set
(dom x0) /\ (left_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng s is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,s)
rng (s ^\ k) is V78() V79() V80() Element of K19(REAL)
x0 /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (x0 /* (s ^\ k)) is V22() V23() ext-real Element of REAL
x0 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* s) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
rng (x0 /* (s ^\ k)) is V78() V79() V80() Element of K19(REAL)
right_open_halfline (lim_in-infty x0) is V78() V79() V80() Element of K19(REAL)
K177((lim_in-infty x0),+infty) is set
(dom f1) /\ (right_open_halfline (lim_in-infty x0)) is V78() V79() V80() Element of K19(REAL)
x is set
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (s ^\ k)) . n is V22() V23() ext-real Element of REAL
(s ^\ k) . n is V22() V23() ext-real Element of REAL
x0 . ((s ^\ k) . n) is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
x0 . (s . (n + k)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not f2 <= b₁ } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= lim_in-infty x0 } is set
(x0 /* s) . (n + k) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (s ^\ k)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* s)
f1 /* ((x0 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* s))
(f1 * x0) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* s)
lim (f1 /* (x0 /* (s ^\ k))) is V22() V23() ext-real Element of REAL
lim ((f1 * x0) /* s) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
lim ((f2 * f1),x0) is V22() V23() ext-real Element of REAL
lim_in+infty f2 is V22() V23() ext-real Element of REAL
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
{x0} is V11() V78() V79() V80() set
(dom (f2 * f1)) \ {x0} is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) \ {x0} is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (f2 /* (f1 /* g)) is V22() V23() ext-real Element of REAL
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim ((f2 * f1) /* g) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
lim ((f2 * f1),x0) is V22() V23() ext-real Element of REAL
lim_in-infty f2 is V22() V23() ext-real Element of REAL
g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim g is V22() V23() ext-real Element of REAL
rng g is V78() V79() V80() Element of K19(REAL)
{x0} is V11() V78() V79() V80() set
(dom (f2 * f1)) \ {x0} is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
(dom f1) \ {x0} is V78() V79() V80() Element of K19(REAL)
f1 /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (f1 /* g) is V78() V79() V80() Element of K19(REAL)
dom f2 is V78() V79() V80() Element of K19(REAL)
f2 /* (f1 /* g) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (f2 /* (f1 /* g)) is V22() V23() ext-real Element of REAL
(f2 * f1) /* g is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim ((f2 * f1) /* g) is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in+infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
lim_in+infty (f1 * x0) is V22() V23() ext-real Element of REAL
lim (f1,(lim_in+infty x0)) is V22() V23() ext-real Element of REAL
f2 is V22() V23() ext-real Element of REAL
right_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(f2,+infty) is set
(dom x0) /\ (right_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng s is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,s)
rng (s ^\ k) is V78() V79() V80() Element of K19(REAL)
x0 /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (x0 /* (s ^\ k)) is V22() V23() ext-real Element of REAL
x0 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* s) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
rng (x0 /* (s ^\ k)) is V78() V79() V80() Element of K19(REAL)
{(lim_in+infty x0)} is V11() V78() V79() V80() set
(dom f1) \ {(lim_in+infty x0)} is V78() V79() V80() Element of K19(REAL)
x is set
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (s ^\ k)) . n is V22() V23() ext-real Element of REAL
(s ^\ k) . n is V22() V23() ext-real Element of REAL
x0 . ((s ^\ k) . n) is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
x0 . (s . (n + k)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= f2 } is set
(x0 /* s) . (n + k) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (s ^\ k)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* s)
f1 /* ((x0 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* s))
(f1 * x0) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* s)
lim (f1 /* (x0 /* (s ^\ k))) is V22() V23() ext-real Element of REAL
lim ((f1 * x0) /* s) is V22() V23() ext-real Element of REAL
x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_in-infty x0 is V22() V23() ext-real Element of REAL
dom x0 is V78() V79() V80() Element of K19(REAL)
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f1 * x0 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f1 * x0) is V78() V79() V80() Element of K19(REAL)
lim_in-infty (f1 * x0) is V22() V23() ext-real Element of REAL
lim (f1,(lim_in-infty x0)) is V22() V23() ext-real Element of REAL
f2 is V22() V23() ext-real Element of REAL
left_open_halfline f2 is V78() V79() V80() Element of K19(REAL)
K177(-infty,f2) is set
(dom x0) /\ (left_open_halfline f2) is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng s is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,s)
rng (s ^\ k) is V78() V79() V80() Element of K19(REAL)
x0 /* (s ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim (x0 /* (s ^\ k)) is V22() V23() ext-real Element of REAL
x0 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng (x0 /* s) is V78() V79() V80() Element of K19(REAL)
dom f1 is V78() V79() V80() Element of K19(REAL)
rng (x0 /* (s ^\ k)) is V78() V79() V80() Element of K19(REAL)
{(lim_in-infty x0)} is V11() V78() V79() V80() set
(dom f1) \ {(lim_in-infty x0)} is V78() V79() V80() Element of K19(REAL)
x is set
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
(x0 /* (s ^\ k)) . n is V22() V23() ext-real Element of REAL
(s ^\ k) . n is V22() V23() ext-real Element of REAL
x0 . ((s ^\ k) . n) is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
x0 . (s . (n + k)) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not f2 <= b₁ } is set
(x0 /* s) . (n + k) is V22() V23() ext-real Element of REAL
f1 /* (x0 /* (s ^\ k)) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(x0 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,x0 /* s)
f1 /* ((x0 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f1 /* (x0 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* (x0 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* (x0 /* s))
(f1 * x0) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f1 * x0) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f1 * x0) /* s)
lim (f1 /* (x0 /* (s ^\ k))) is V22() V23() ext-real Element of REAL
lim ((f1 * x0) /* s) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
lim ((f2 * f1),x0) is V22() V23() ext-real Element of REAL
lim_left (f2,(lim (f1,x0))) is V22() V23() ext-real Element of REAL
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
{x0} is V11() V78() V79() V80() set
(dom (f2 * f1)) \ {x0} is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 + g <= b₁ ) } is set
].(x0 - g),(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),(x0 + g).[ \ {x0} is V78() V79() V80() Element of K19(REAL)
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not lim (f1,x0) <= b₁ } is set
left_open_halfline (lim (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177(-infty,(lim (f1,x0))) is set
dom f2 is V78() V79() V80() Element of K19(REAL)
(dom f2) /\ (left_open_halfline (lim (f1,x0))) is V78() V79() V80() Element of K19(REAL)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) \ {x0} is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
lim (f2 /* ((f1 /* s) ^\ k)) is V22() V23() ext-real Element of REAL
lim ((f2 * f1) /* s) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_left (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
lim_left ((f2 * f1),x0) is V22() V23() ext-real Element of REAL
lim (f2,(lim_left (f1,x0))) is V22() V23() ext-real Element of REAL
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
left_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(-infty,x0) is set
(dom (f2 * f1)) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not x0 <= b₁ } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{(lim_left (f1,x0))} is V11() V78() V79() V80() set
dom f2 is V78() V79() V80() Element of K19(REAL)
(dom f2) \ {(lim_left (f1,x0))} is V78() V79() V80() Element of K19(REAL)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (left_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
lim (f2 /* ((f1 /* s) ^\ k)) is V22() V23() ext-real Element of REAL
lim ((f2 * f1) /* s) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
lim ((f2 * f1),x0) is V22() V23() ext-real Element of REAL
lim_right (f2,(lim (f1,x0))) is V22() V23() ext-real Element of REAL
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
{x0} is V11() V78() V79() V80() set
(dom (f2 * f1)) \ {x0} is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 + g <= b₁ ) } is set
].(x0 - g),(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),(x0 + g).[ \ {x0} is V78() V79() V80() Element of K19(REAL)
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= lim (f1,x0) } is set
right_open_halfline (lim (f1,x0)) is V78() V79() V80() Element of K19(REAL)
K177((lim (f1,x0)),+infty) is set
dom f2 is V78() V79() V80() Element of K19(REAL)
(dom f2) /\ (right_open_halfline (lim (f1,x0))) is V78() V79() V80() Element of K19(REAL)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) \ {x0} is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
lim (f2 /* ((f1 /* s) ^\ k)) is V22() V23() ext-real Element of REAL
lim ((f2 * f1) /* s) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim_right (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
lim_right ((f2 * f1),x0) is V22() V23() ext-real Element of REAL
lim (f2,(lim_right (f1,x0))) is V22() V23() ext-real Element of REAL
g is V22() V23() ext-real Element of REAL
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
right_open_halfline x0 is V78() V79() V80() Element of K19(REAL)
K177(x0,+infty) is set
(dom (f2 * f1)) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : not b₁ <= x0 } is set
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 & not x0 + g <= b₁ ) } is set
c₁₀ is V22() V23() ext-real Element of REAL
{(lim_right (f1,x0))} is V11() V78() V79() V80() set
dom f2 is V78() V79() V80() Element of K19(REAL)
(dom f2) \ {(lim_right (f1,x0))} is V78() V79() V80() Element of K19(REAL)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) /\ (right_open_halfline x0) is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
lim (f2 /* ((f1 /* s) ^\ k)) is V22() V23() ext-real Element of REAL
lim ((f2 * f1) /* s) is V22() V23() ext-real Element of REAL
x0 is V22() V23() ext-real Element of REAL
f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
lim (f1,x0) is V22() V23() ext-real Element of REAL
dom f1 is V78() V79() V80() Element of K19(REAL)
f2 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
f2 * f1 is V1() V4( REAL ) V5( REAL ) V6() V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (f2 * f1) is V78() V79() V80() Element of K19(REAL)
lim ((f2 * f1),x0) is V22() V23() ext-real Element of REAL
lim (f2,(lim (f1,x0))) is V22() V23() ext-real Element of REAL
g is V22() V23() ext-real Element of REAL
x0 - g is V22() V23() ext-real Element of REAL
].(x0 - g),x0.[ is V78() V79() V80() Element of K19(REAL)
x0 + g is V22() V23() ext-real Element of REAL
].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),x0.[ \/ ].x0,(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
(dom f1) /\ (].(x0 - g),x0.[ \/ ].x0,(x0 + g).[) is V78() V79() V80() Element of K19(REAL)
s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim s is V22() V23() ext-real Element of REAL
rng s is V78() V79() V80() Element of K19(REAL)
{x0} is V11() V78() V79() V80() set
(dom (f2 * f1)) \ {x0} is V78() V79() V80() Element of K19(REAL)
k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
f1 /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f1 /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f1 /* s)
x is set
rng ((f1 /* s) ^\ k) is V78() V79() V80() Element of K19(REAL)
n is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
((f1 /* s) ^\ k) . n is V22() V23() ext-real Element of REAL
n + k is V15() V16() V17() V21() V22() V23() ext-real V78() V79() V80() V81() V82() V83() Element of NAT
s . (n + k) is V22() V23() ext-real Element of REAL
f1 . (s . (n + k)) is V22() V23() ext-real Element of REAL
(f1 /* s) . (n + k) is V22() V23() ext-real Element of REAL
{ b₁ where b₁ is V22() V23() ext-real Element of REAL : ( not b₁ <= x0 - g & not x0 + g <= b₁ ) } is set
].(x0 - g),(x0 + g).[ is V78() V79() V80() Element of K19(REAL)
].(x0 - g),(x0 + g).[ \ {x0} is V78() V79() V80() Element of K19(REAL)
{(lim (f1,x0))} is V11() V78() V79() V80() set
dom f2 is V78() V79() V80() Element of K19(REAL)
(dom f2) \ {(lim (f1,x0))} is V78() V79() V80() Element of K19(REAL)
rng (f1 /* s) is V78() V79() V80() Element of K19(REAL)
f2 /* ((f1 /* s) ^\ k) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
f2 /* (f1 /* s) is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(f2 /* (f1 /* s)) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,f2 /* (f1 /* s))
(f2 * f1) /* s is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
((f2 * f1) /* s) ^\ k is V1() V4( NAT ) V5( REAL ) V6() V11() total quasi_total V33() V34() V35() M7( REAL ,(f2 * f1) /* s)
(dom f1) \ {x0} is V78() V79() V80() Element of K19(REAL)
lim (f1 /* s) is V22() V23() ext-real Element of REAL
lim ((f1 /* s) ^\ k) is V22() V23() ext-real Element of REAL
lim (f2 /* ((f1 /* s) ^\ k)) is V22() V23() ext-real Element of REAL
lim ((f2 * f1) /* s) is V22() V23() ext-real Element of REAL