theorem Th39: :: CAT_6:38

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