for C being composable with_identities CategoryStr
for f, g being Element of Mor C st (SourceMap C) . g = (TargetMap C) . f holds
( (SourceMap C) . ((CompMap C) . (g,f)) = (SourceMap C) . f & (TargetMap C) . ((CompMap C) . (g,f)) = (TargetMap C) . g )