:: deftheorem defines 0_fs_Zero LMODFREE:def 12 :
for R being Ring
for X being set holds 0_fs_Zero (X,R) = 0_Funcs (X,R);