:: deftheorem defines RealFuncZero FUNCSDOM:def 4 :
for A being set holds RealFuncZero A = A --> 0;