theorem Th9: :: CAT_4:9

for o, m being set
for c being Object of (c1Cat (o,m))
for p1, p2 being Morphism of (c1Cat (o,m)) holds c is_a_product_wrt p1,p2