:: deftheorem Def10 defines * MOD_2:def 10 :
for R being Ring
for G, F being LModMorphism of R st dom G = cod F holds
for b₄ being strict LModMorphism of R holds
( b₄ = G * F iff for G1, G2, G3 being LeftMod of R
for g being Function of G2,G3
for f being Function of G1,G2 st LModMorphismStr(# the Dom of G, the Cod of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the Dom of F, the Cod of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
b₄ = LModMorphismStr(# G1,G3,(g * f) #) );