:: deftheorem Def20 defines Obj CAT_1:def 22 :
for C, D being Category
for F being Function of the carrier' of C, the carrier' of D st ( for c being Element of C ex d being Element of D st F . (id c) = id d ) holds
for b₄ being Function of the carrier of C, the carrier of D holds
( b₄ = Obj F iff for c being Element of C
for d being Element of D st F . (id c) = id d holds
b₄ . c = d );