:: deftheorem defines isomorphic ISOCAT_1:def 3 :
for A, B being Category
for F being Functor of A,B holds
( F is isomorphic iff ( F is one-to-one & rng F = the carrier' of B ) );