g (*) f in Hom (a,c) by A1, Th19;
hence g (*) f is Morphism of a,c by Def3; :: thesis: verum