:: deftheorem defines add_Hom LMOD_XX1:def 19 :
for R being comRing
for M, N being LeftMod of R holds add_Hom (M,N) = (ADD (M,N)) | [:(set_Hom (M,N)),(set_Hom (M,N)):];