:: deftheorem defines RealFuncUnit FUNCSDOM:def 5 :
for A being set holds RealFuncUnit A = A --> 1;