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