theorem :: CAT_3:46

for I being set
for C being Category
for a being Object of C
for F being Function of I, the carrier' of C
for G being Projections_family of a,I st doms F = cods G holds
F "*" G is Projections_family of a,I