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