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