deffunc H₁( 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₁(f) from FUNCT_2:sch 4(); :: thesis: verum