let C be non empty set ; :: thesis: for g being PartFunc of C,COMPLEX holds
( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) )
let g be PartFunc of C,COMPLEX; :: thesis: ( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) )
dom (g ^) = (dom g) \ (g " {0c}) by Def2;
hence dom (g ^) c= dom g by XBOOLE_1:36; :: 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, XBOOLE_1:36; :: thesis: verum