theorem Th71: :: VALUED_2:71
for X being set
for Y being complex-functions-membered set
for f being PartFunc of X,Y
for g being complex-valued Function holds dom (f </> g) = (dom f) /\ (dom g)