:: deftheorem Def10 defines /. CAT_3:def 10 :
for C being Category
for a, b being Object of C st Hom (a,b) <> {} holds
for D being Category
for T being Functor of C,D
for f being Morphism of a,b holds T /. f = T . f;