theorem Th6: :: CAT_3:6

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