let R be Ring; :: thesis: for f, g being strict LModMorphism of R st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g )
let f, g be strict LModMorphism of R; :: thesis: ( dom g = cod f implies ( dom (g * f) = dom f & cod (g * f) = cod g ) )
assume dom g = cod f ; :: thesis: ( dom (g * f) = dom f & cod (g * f) = cod g )
then A1: ex G1, G2, G3 being LeftMod of R ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = LModMorphismStr(# G1,G2,f0 #) & g = LModMorphismStr(# G2,G3,g0 #) & g * f = LModMorphismStr(# G1,G3,(g0 * f0) #) ) by Th14;
hence dom (g * f) = dom f ; :: thesis: cod (g * f) = cod g
thus cod (g * f) = cod g by A1; :: thesis: verum