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 f' = f as strict Element of Morphs (LModObjects UN,R) by Th15;
reconsider g' = g as strict Element of Morphs (LModObjects UN,R) by Th15;
A2: dom g' = cod f' by A1, Th18;
then A3: ( dom (g' * f') = dom f' & cod (g' * f') = cod g' ) by MOD_2:23;
reconsider gf = g' * f' as Element of Morphs (LModObjects UN,R) by A2, Th12;
gf = g * f by A1, Th18;
hence ( dom (g * f) = dom f & cod (g * f) = cod g ) by A3, Th18; :: thesis: verum