theorem :: CAT_5:25

for C being Category
for a, b being Object of C holds Hom (a,b) = (a Hom) /\ (Hom b)