theorem Th22: :: CAT_2:28
for C, D being Category
for f being Morphism of C
for g being Morphism of D holds
( dom [f,g] = [(dom f),(dom g)] & cod [f,g] = [(cod f),(cod g)] )