for C, D being with_identities CategoryStr st C ~= D holds
( card (Mor C) = card (Mor D) & card (Ob C) = card (Ob D) )