theorem Th19: :: CAT_6:19

for C being CategoryStr holds
( C is with_right_identities iff CategoryStr(# the carrier of C, the composition of C #) is with_right_identities )