theorem
Th39
:
:: SUPINF_2:40
for
F
being
sequence
of
ExtREAL
for
n
being
Nat
st
F
is
nonnegative
holds
(
(
Ser
F
)
.
n
<=
(
Ser
F
)
.
(
n
+
1
)
&
0.
<=
(
Ser
F
)
.
n
)