:: deftheorem defines lmult_Hom LMOD_XX1:def 20 :
for R being comRing
for M, N being LeftMod of R holds lmult_Hom (M,N) = (LMULT (M,N)) | [: the carrier of R,(set_Hom (M,N)):];