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