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 that
A1: f in Hom a,b and
A2: g in Hom b,c ; :: thesis: (Den (compsym a,b,c),(MSAlg C)) . <*g,f*> = g * f
A3: ( dom g = b & cod g = c ) by A2, CAT_1:18;
( dom f = a & cod f = b ) by A1, CAT_1:18;
hence (Den (compsym a,b,c),(MSAlg C)) . <*g,f*> = g * f by A3, Def15; :: thesis: verum