deffunc H_{1}( Morphism of C) -> Element of the carrier' of B = S . ($1 opp);

thus ex F being Function of the carrier' of C, the carrier' of B st

for f being Morphism of C holds F . f = H_{1}(f)
from FUNCT_2:sch 4(); :: thesis: verum

thus ex F being Function of the carrier' of C, the carrier' of B st

for f being Morphism of C holds F . f = H