let C be Category; :: thesis: 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
let a, b, c be Object of C; :: thesis: 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
let f, g be Morphism of C; :: thesis: ( f in Hom a,b & g in Hom b,c implies (Den (compsym a,b,c),(MSAlg C)) . <*g,f*> = g * f )
assume ( f in Hom a,b & g in Hom b,c ) ; :: thesis: (Den (compsym a,b,c),(MSAlg C)) . <*g,f*> = g * f
then ( dom f = a & cod f = b & dom g = b & cod g = c ) by CAT_1:18;
hence (Den (compsym a,b,c),(MSAlg C)) . <*g,f*> = g * f by Def15; :: thesis: verum