theorem :: FUNCSDOM:3

for A being non empty set holds RealFuncZero A <> RealFuncUnit A