:: deftheorem Def19 defines cod CAT_6:def 19 :
for C being composable with_identities CategoryStr
for f being morphism of C
for b₃ being Object of C holds
( ( not C is empty implies ( b₃ = cod f iff ex f1 being morphism of C st
( b₃ = f1 & f1 |> f & f1 is identity ) ) ) & ( C is empty implies ( b₃ = cod f iff b₃ = the Object of C ) ) );