:: deftheorem defines Func_Mod LMOD_XX1:def 17 :
for R being Ring
for M, N being LeftMod of R holds Func_Mod (R,M,N) = ModuleStr(# (Funcs ( the carrier of M, the carrier of N)),(ADD (M,N)),(0_Funcs (M,N)),(LMULT (M,N)) #);