theorem Th31: :: CATALG_1:31

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