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