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