deffunc
H
_{1}
(
Morphism
of
(
C
opp
)
)
->
Element
of the
carrier'
of
B
=
S
.
(
opp
$1
)
;
thus
ex
F
being
Function
of the
carrier'
of
(
C
opp
)
, the
carrier'
of
B
st
for
f
being
Morphism
of
(
C
opp
)
holds
F
.
f
=
H
_{1}
(
f
)
from
FUNCT_2:sch 4
();
:: thesis:
verum