let g be complex-valued Function; :: thesis: ( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) )
dom (g ^) = (dom g) \ (g " {0}) by Def2;
hence dom (g ^) c= dom g ; :: thesis: (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0})
thus (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) by XBOOLE_1:28; :: thesis: verum