theorem Th3: :: ALGSPEC1:3

for f, g, h being Function st dom f misses rng h & g .: (dom h) misses dom f holds
f * (g +* h) = f * g