theorem
:: SUPINF_2:33
for
X
being non
empty
set
for
Y
,
Z
being non
empty
Subset
of
ExtREAL
for
F1
being
Function
of
X
,
Y
for
F2
being
Function
of
X
,
Z
st
F1
is
bounded
&
F2
is
bounded
holds
F1
+
F2
is
bounded
by
Th31
,
Th30
;