let f be non-empty real-valued Function; :: thesis: dom (f ^) = dom f
thus dom (f ^) = (dom f) \ (f " {0}) by RFUNCT_1:def 2
.= dom f ; :: thesis: verum