let f, g, h be strict GroupMorphism; :: 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
set G2 = cod f;
set G3 = cod g;
reconsider h9 = h as Morphism of cod g, cod h by A1, Def12;
reconsider g9 = g as Morphism of cod f, cod g by A2, Def12;
reconsider f9 = f as Morphism of dom f, cod f by Def12;
h9 * (g9 * f9) = (h9 * g9) * f9 by Th21;
hence h * (g * f) = (h * g) * f ; :: thesis: verum