theorem Th14: :: CAT_3:14

for x1, x2 being set
for C being Category
for f, p1, p2 being Morphism of C st x1 <> x2 holds
((x1,x2) --> (p1,p2)) * f = (x1,x2) --> ((p1 (*) f),(p2 (*) f))