for R being Ring
for G1, G2 being LeftMod of R
for f being LModMorphismStr over R
for f0 being Function of G1,G2 st f = LModMorphismStr(# G1,G2,f0 #) holds
( dom f = G1 & cod f = G2 & fun f = f0 ) ;