theorem Th10: :: RINGCAT1:10
for f, g, h being strict RingMorphism st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f