theorem Th50: :: CAT_3:50

for C being Category
for a being Object of C
for F being Function of {}, the carrier' of C holds
( a is_a_product_wrt F iff a is terminal )