theorem Th27: :: CATALG_1:27

for A being Category
for a, b, c being Object of A holds
( Args ((compsym (a,b,c)),(MSAlg A)) = product <*(Hom (b,c)),(Hom (a,b))*> & Result ((compsym (a,b,c)),(MSAlg A)) = Hom (a,c) )