:: deftheorem defines Func_Mod LMODFREE:def 4 :
for R being Ring
for X being set
for N being LeftMod of R holds Func_Mod (X,N) = ModuleStr(# (Funcs (X, the carrier of N)),(ADD (X,N)),(0_Funcs (X,N)),(LMULT (X,N)) #);