let UN be Universe; :: thesis: for R being Ring
for f, g, h being Morphism of (LModCat UN,R) st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f
let R be Ring; :: thesis: for f, g, h being Morphism of (LModCat UN,R) st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f
set X = Morphs (LModObjects UN,R);
let f, g, h be Morphism of (LModCat UN,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
reconsider f' = f, g' = g, h' = h as strict Element of Morphs (LModObjects UN,R) by Th15;
A2: ( dom h' = cod g' & dom g' = cod f' ) by A1, Th18;
A3: ( g' * f' = g * f & h' * g' = h * g ) by A1, Th18;
reconsider gf = g' * f', hg = h' * g' as strict Element of Morphs (LModObjects UN,R) by A2, Th12;
A4: dom h = cod (g * f) by A1, Lm1;
A5: dom (h * g) = cod f by A1, Lm1;
h * (g * f) = h' * gf by A3, A4, Th18
.= hg * f' by A2, MOD_2:25
.= (h * g) * f by A3, A5, Th18 ;
hence h * (g * f) = (h * g) * f ; :: thesis: verum