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 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 strict Morphism of cod g, cod h by A1, Def8;

reconsider g9 = g as strict Morphism of cod f, cod g by A2, Def8;

reconsider f9 = f as strict Morphism of dom f, cod f by Def8;

h9 * (g9 * f9) = (h9 * g9) * f9 by Th16;

hence h * (g * f) = (h * g) * f ; :: thesis: verum

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 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 strict Morphism of cod g, cod h by A1, Def8;

reconsider g9 = g as strict Morphism of cod f, cod g by A2, Def8;

reconsider f9 = f as strict Morphism of dom f, cod f by Def8;

h9 * (g9 * f9) = (h9 * g9) * f9 by Th16;

hence h * (g * f) = (h * g) * f ; :: thesis: verum