:: deftheorem Def19 defines Functor CAT_1:def 21 :
for C, D being Category
for b₃ being Function of the carrier' of C, the carrier' of D holds
( b₃ is Functor of C,D iff ( ( for c being Element of C ex d being Element of D st b₃ . (id c) = id d ) & ( for f being Element of the carrier' of C holds
( b₃ . (id (dom f)) = id (dom (b₃ . f)) & b₃ . (id (cod f)) = id (cod (b₃ . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
b₃ . (g (*) f) = (b₃ . g) (*) (b₃ . f) ) ) );