:: deftheorem defines isomorphic CAT_1:def 25 :
for C, D being Category
for T being Functor of C,D holds
( T is isomorphic iff ( T is one-to-one & rng T = the carrier' of D & rng (Obj T) = the carrier of D ) );