theorem Th2: :: ALGSPEC1:2

for f, g, h being Function st f c= g & (rng h) /\ (dom g) c= dom f holds
g * h = f * h