:: deftheorem defines FS_Funcs LMODFREE:def 13 :
for R being Ring
for X being set holds FS_Funcs (X,R) = ModuleStr(# (fs_Funcs (X,R)),(fs_ADD (X,R)),(0_fs_Zero (X,R)),(fs_LMULT (X,R)) #);