:: deftheorem Def5 defines * CAT_3:def 5 :
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 /. x) (*) f );