:: deftheorem Def18 defines dom CAT_6:def 18 :
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₃ = dom f iff ex f1 being morphism of C st
( b₃ = f1 & f |> f1 & f1 is identity ) ) ) & ( C is empty implies ( b₃ = dom f iff b₃ = the Object of C ) ) );