theorem Th1: :: RFUNCT_1:1

for g being complex-valued Function holds
( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) )