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 f9 = f, g9 = g, h9 = h as strict Element of Morphs (LModObjects (UN,R)) ;
A2: ( h9 * g9 = h (*) g & dom (h (*) g) = cod f ) by A1, Lm1, Th14;
A3: ( dom h9 = cod g9 & dom g9 = cod f9 ) by A1, Th14;
then reconsider gf = g9 * f9, hg = h9 * g9 as strict Element of Morphs (LModObjects (UN,R)) by Th10;
( g9 * f9 = g (*) f & dom h = cod (g (*) f) ) by A1, Lm1, Th14;
then h (*) (g (*) f) = h9 * gf by Th14
.= hg * f9 by A3, MOD_2:17
.= (h (*) g) (*) f by A2, Th14 ;
hence h (*) (g (*) f) = (h (*) g) (*) f ; :: thesis: verum