:: 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 DomL of G, the CodL of G, the Fun of G #) = LModMorphismStr(# G2,G3,g #) & LModMorphismStr(# the DomL of F, the CodL of F, the Fun of F #) = LModMorphismStr(# G1,G2,f #) holds
b₄ = LModMorphismStr(# G1,G3,(g * f) #) );