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