theorem Th1: :: AOFA_000:1

for f, g, h being Function
for A being set st A c= dom f & A c= dom g & rng h c= A & ( for x being set st x in A holds
f . x = g . x ) holds
f * h = g * h