for I being set
for C being Category
for F, G being Function of I, the carrier' of C st doms F = cods G holds
( doms (F "*" G) = doms G & cods (F "*" G) = cods F )