let C, D be empty with_identities CategoryStr ; :: thesis: C ~= D

set F = the covariant Functor of C,D;

set G = the covariant Functor of D,C;

( the covariant Functor of D,C (*) the covariant Functor of C,D = id C & the covariant Functor of C,D (*) the covariant Functor of D,C = id D ) ;

hence C ~= D by CAT_6:def 28; :: thesis: verum

set F = the covariant Functor of C,D;

set G = the covariant Functor of D,C;

( the covariant Functor of D,C (*) the covariant Functor of C,D = id C & the covariant Functor of C,D (*) the covariant Functor of D,C = id D ) ;

hence C ~= D by CAT_6:def 28; :: thesis: verum