theorem Th22: :: GRCAT_1:22

for f, g, h being strict GroupMorphism st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f