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