:: deftheorem defines isomorphism CAT_7:def 19 :
for C, D being category
for F being Functor of C,D holds
( F is isomorphism iff ( F is covariant & ex G being Functor of D,C st
( G is covariant & G (*) F = id C & F (*) G = id D ) ) );