theorem :: ENS_1:55

for C being Category
for f, g being Morphism of C holds hom (f,g) = (hom ((dom f),g)) * (hom (f,(dom g)))