theorem Th16: :: VALUED_1:16

for f1, f2 being complex-valued Function holds dom (f1 /" f2) = (dom f1) /\ (dom f2)