for C being non empty composable with_identities CategoryStr
for f, g being Element of Mor C holds
( [g,f] in dom (CompMap C) iff (SourceMap C) . g = (TargetMap C) . f )