theorem :: AOFA_A00:4

for f, g being Function-yielding Function holds doms (f * g) = (doms f) * g