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