let R be Ring; :: thesis: for f, g, h being strict LModMorphism of R st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f
let f, g, h be strict LModMorphism of R; :: thesis: ( dom h = cod g & dom g = cod f implies h * (g * f) = (h * g) * f )
assume A1: ( dom h = cod g & dom g = cod f ) ; :: thesis: h * (g * f) = (h * g) * f
set G2 = cod f;
set G3 = cod g;
reconsider f' = f as strict Morphism of dom f, cod f by Def11;
reconsider g' = g as strict Morphism of cod f, cod g by A1, Def11;
reconsider h' = h as strict Morphism of cod g, cod h by A1, Def11;
h' * (g' * f') = (h' * g') * f' by Th24;
hence h * (g * f) = (h * g) * f ; :: thesis: verum