theorem
Th42
:
:: SUPINF_2:43
for
F1
,
F2
being
sequence
of
ExtREAL
st ( for
n
being
Element
of
NAT
holds
F1
.
n
<=
F2
.
n
) holds
SUM
F1
<=
SUM
F2