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