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