theorem Th42: :: CAT_3:42

for C being Category
for a being Object of C
for F being Function of {}, the carrier' of C holds F is Projections_family of a, {}