:: deftheorem Def6 defines * CAT_3:def 6 :
for C being Category
for I being set
for F being Function of I, the carrier' of C
for f being Morphism of C
for b₅ being Function of I, the carrier' of C holds
( b₅ = f * F iff for x being set st x in I holds
b₅ /. x = f (*) (F /. x) );