theorem Th9: :: ISOCAT_2:11

for A, B being Category
for a1, a2 being Object of A
for b1, b2 being Object of B holds
( ( Hom (a1,a2) <> {} & Hom (b1,b2) <> {} ) iff Hom ([a1,b1],[a2,b2]) <> {} )