for C being composable with_identities CategoryStr holds
( dom (RelOb C) = Ob C & rng (RelOb C) = Ob C )