::
deftheorem
Def4
defines

SUPINF_2:def 4 :
for
X
being non
empty
set
for
Y
being non
empty
Subset
of
ExtREAL
for
F
being
Function
of
X
,
Y
for
b
_{4}
being
Function
of
X
,
(

Y
)
holds
(
b
_{4}
=

F
iff for
x
being
Element
of
X
holds
b
_{4}
.
x
=

(
F
.
x
)
);