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 consider G1, G2, G3 being LeftMod of R, f0 being Function of G1,G2, g0 being Function of G2,G3 such that
A1: ( f = LModMorphismStr(# G1,G2,f0 #) & g = LModMorphismStr(# G2,G3,g0 #) & g * f = LModMorphismStr(# G1,G3,(g0 * f0) #) ) by Th22;
thus dom (g * f) = dom f by A1; :: thesis: cod (g * f) = cod g
thus cod (g * f) = cod g by A1; :: thesis: verum