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:18;
A5: (Den (compsym b,c,d),(MSAlg C)) . <*h,g*> = h * g by A2, A3, Th42;
A6: cod f = b by A1, CAT_1:18;
A7: dom h = c by A3, CAT_1:18;
cod h = d by A3, CAT_1:18;
then A8: cod (h * g) = d by A4, A7, CAT_1:42;
A9: dom g = b by A2, CAT_1:18;
then dom (h * g) = b by A4, A7, CAT_1:42;
then A10: h * g in Hom b,d by A8, CAT_1:18;
dom f = a by A1, CAT_1:18;
then A11: dom (g * f) = a by A6, A9, CAT_1:42;
cod (g * f) = c by A6, A9, A4, CAT_1:42;
then A12: g * f in Hom a,c by A11, CAT_1:18;
(Den (compsym a,b,c),(MSAlg C)) . <*g,f*> = g * f by A1, A2, Th42;
hence (Den (compsym a,c,d),(MSAlg C)) . <*h,((Den (compsym a,b,c),(MSAlg C)) . <*g,f*>)*> = h * (g * f) by A3, A12, Th42
.= (h * g) * f by A6, A9, A4, A7, CAT_1:43
.= (Den (compsym a,b,d),(MSAlg C)) . <*((Den (compsym b,c,d),(MSAlg C)) . <*h,g*>),f*> by A1, A5, A10, Th42 ;
:: thesis: verum