theorem :: CATALG_1:32

for C being Category
for a, b, c, d being Object of C
for f, g, h being Morphism of C st f in Hom (a,b) & g in Hom (b,c) & h in Hom (c,d) holds
(Den ((compsym (a,c,d)),(MSAlg C))) . <*h,((Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*>)*> = (Den ((compsym (a,b,d)),(MSAlg C))) . <*((Den ((compsym (b,c,d)),(MSAlg C))) . <*h,g*>),f*>