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