let f, g, h be strict RingMorphism; :: 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 G1 = dom f;
set G2 = cod f;
set G3 = cod g;
set G4 = cod h;
reconsider h' = h as Morphism of cod g, cod h by A1, Th6;
reconsider f' = f as Morphism of dom f, cod f by Th6;
reconsider g' = g as Morphism of cod f, cod g by A2, Th6;
A3: dom f <= cod f by Th6;
( cod f <= cod g & cod g <= cod h ) by A1, A2, Th6;
then h' * (g' * f') = (h' * g') * f' by A3, Th12;
hence h * (g * f) = (h * g) * f ; :: thesis: verum