theorem Th2: :: RFUNCT_1:2

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