:: deftheorem defines Hom LMOD_XX1:def 22 :
for R being comRing
for M, N being LeftMod of R holds Hom (R,M,N) = ModuleStr(# (set_Hom (M,N)),(add_Hom (M,N)),(0_Hom (M,N)),(lmult_Hom (M,N)) #);