theorem Th40: :: CAT_6:39

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