theorem Th12: :: ISOCAT_2:14

for A, B being Category
for a1, a2 being Object of A
for b1, b2 being Object of B
for f being Morphism of A
for g being Morphism of B st f in Hom (a1,a2) & g in Hom (b1,b2) holds
[f,g] in Hom ([a1,b1],[a2,b2])