theorem :: PARTFUN1:79

for f1, f2, g being Function st rng g c= dom f1 & rng g c= dom f2 & f1 tolerates f2 holds
f1 * g = f2 * g