let C be Category; :: thesis: for f being Morphism of C
for g being Element of (cod f) Hom holds g (*) f in (dom f) Hom
let f be Morphism of C; :: thesis: for g being Element of (cod f) Hom holds g (*) f in (dom f) Hom
let g be Element of (cod f) Hom ; :: thesis: g (*) f in (dom f) Hom
cod f = dom g by Th24;
then dom (g (*) f) = dom f by CAT_1:17;
hence g (*) f in (dom f) Hom by Th24; :: thesis: verum