let C be Category; :: thesis: for a, b, c, d being Object of C
for f, g, h being Morphism of C st f in Hom (a,b) & g in Hom (b,c) & h in Hom (c,d) holds
(Den ((compsym (a,c,d)),(MSAlg C))) . <*h,((Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*>)*> = (Den ((compsym (a,b,d)),(MSAlg C))) . <*((Den ((compsym (b,c,d)),(MSAlg C))) . <*h,g*>),f*>
let a, b, c, d be Object of C; :: thesis: for f, g, h being Morphism of C st f in Hom (a,b) & g in Hom (b,c) & h in Hom (c,d) holds
(Den ((compsym (a,c,d)),(MSAlg C))) . <*h,((Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*>)*> = (Den ((compsym (a,b,d)),(MSAlg C))) . <*((Den ((compsym (b,c,d)),(MSAlg C))) . <*h,g*>),f*>
let f, g, h be Morphism of C; :: thesis: ( f in Hom (a,b) & g in Hom (b,c) & h in Hom (c,d) implies (Den ((compsym (a,c,d)),(MSAlg C))) . <*h,((Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*>)*> = (Den ((compsym (a,b,d)),(MSAlg C))) . <*((Den ((compsym (b,c,d)),(MSAlg C))) . <*h,g*>),f*> )
assume that
A1: f in Hom (a,b) and
A2: g in Hom (b,c) and
A3: h in Hom (c,d) ; :: thesis: (Den ((compsym (a,c,d)),(MSAlg C))) . <*h,((Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*>)*> = (Den ((compsym (a,b,d)),(MSAlg C))) . <*((Den ((compsym (b,c,d)),(MSAlg C))) . <*h,g*>),f*>
A4: cod g = c by A2, CAT_1:1;
A5: (Den ((compsym (b,c,d)),(MSAlg C))) . <*h,g*> = h (*) g by A2, A3, Th31;
A6: cod f = b by A1, CAT_1:1;
A7: dom h = c by A3, CAT_1:1;
cod h = d by A3, CAT_1:1;
then A8: cod (h (*) g) = d by A4, A7, CAT_1:17;
A9: dom g = b by A2, CAT_1:1;
then dom (h (*) g) = b by A4, A7, CAT_1:17;
then A10: h (*) g in Hom (b,d) by A8;
dom f = a by A1, CAT_1:1;
then A11: dom (g (*) f) = a by A6, A9, CAT_1:17;
cod (g (*) f) = c by A6, A9, A4, CAT_1:17;
then A12: g (*) f in Hom (a,c) by A11;
(Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*> = g (*) f by A1, A2, Th31;
hence (Den ((compsym (a,c,d)),(MSAlg C))) . <*h,((Den ((compsym (a,b,c)),(MSAlg C))) . <*g,f*>)*> = h (*) (g (*) f) by A3, A12, Th31
.= (h (*) g) (*) f by A6, A9, A4, A7, CAT_1:18
.= (Den ((compsym (a,b,d)),(MSAlg C))) . <*((Den ((compsym (b,c,d)),(MSAlg C))) . <*h,g*>),f*> by A1, A5, A10, Th31 ;
:: thesis: verum