let UN be Universe; :: thesis: for R being Ring
for f, g being Morphism of (LModCat (UN,R)) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
let R be Ring; :: thesis: for f, g being Morphism of (LModCat (UN,R)) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
set X = Morphs (LModObjects (UN,R));
let f, g be Morphism of (LModCat (UN,R)); :: thesis: ( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
assume A1: dom g = cod f ; :: thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
reconsider g9 = g as strict Element of Morphs (LModObjects (UN,R)) ;
reconsider f9 = f as strict Element of Morphs (LModObjects (UN,R)) ;
A2: dom g9 = cod f9 by A1, Th14;
then A3: ( dom (g9 * f9) = dom f9 & cod (g9 * f9) = cod g9 ) by MOD_2:15;
reconsider gf = g9 * f9 as Element of Morphs (LModObjects (UN,R)) by A2, Th10;
gf = g (*) f by A1, Th14;
hence ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A3, Th14; :: thesis: verum