theorem :: CAT_3:52

for y being set
for C being Category
for a being Object of C holds a is_a_product_wrt y .--> (id a)