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 Def8;
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