:: deftheorem defines fs_ADD LMODFREE:def 10 :
for R being Ring
for X being set holds fs_ADD (X,R) = (ADD (X,R)) | [:(fs_Funcs (X,R)),(fs_Funcs (X,R)):];