deffunc
H
_{1}
(
Subset
of
X
)
->
Element
of
ExtREAL
=
inf
(
Svc
(
M
,$1)
)
;
thus
for
F1
,
F2
being
Function
of
(
bool
X
)
,
ExtREAL
st ( for
A
being
Subset
of
X
holds
F1
.
A
=
H
_{1}
(
A
) ) & ( for
A
being
Subset
of
X
holds
F2
.
A
=
H
_{1}
(
A
) ) holds
F1
=
F2
from
BINOP_2:sch 1
();
:: thesis:
verum