:: deftheorem defines *' MOD_2:def 11 :
for R being Ring
for G1, G2, G3 being LeftMod of R
for G being Morphism of G2,G3
for F being Morphism of G1,G2 holds G *' F = G * F;