thus
ex
f
being
Function
of
X
,
T
st
for
x
being
Element
of
X
holds
f
.
x
=
H
_{1}
(
x
)
from
FUNCT_2:sch 4
();
:: thesis:
verum