let C be Category; :: thesis: for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f
let f, g, h be Morphism of C; :: thesis: ( dom h = cod g & dom g = cod f implies h * (g * f) = (h * g) * f )
assume that
A1: dom h = cod g and
A2: dom g = cod f ; :: thesis: h * (g * f) = (h * g) * f
cod (g * f) = cod g by A2, Th42;
then A3: the Comp of C . (h,(g * f)) = h * (g * f) by A1, Th41;
dom (h * g) = dom g by A1, Th42;
then A4: the Comp of C . ((h * g),f) = (h * g) * f by A2, Th41;
( the Comp of C . (h,g) = h * g & the Comp of C . (g,f) = g * f ) by A1, A2, Th41;
hence h * (g * f) = (h * g) * f by A1, A2, A3, A4, Def8; :: thesis: verum