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