theorem :: CAT_2:33

for C, D being Category
for c, c9 being Object of C
for f being Morphism of c,c9
for d, d9 being Object of D
for g being Morphism of d,d9 st Hom (c,c9) <> {} & Hom (d,d9) <> {} holds
[f,g] is Morphism of [c,d],[c9,d9]