for C being composable with_identities CategoryStr
for f, f1 being morphism of C st f |> f1 & f1 is identity holds
dom f = f1