theorem Th6: :: CFUNCT_1:6

for C being non empty set
for g being PartFunc of C,COMPLEX holds
( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) )