theorem Th7: :: CAT_3:7

for x1, x2 being set
for C being Category
for p1, p2 being Morphism of C holds cods ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((cod p1),(cod p2))