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