theorem Th23: :: TOPS_5:23

for f, g being non-empty Function st dom g c= dom f & ( for i being object st i in dom g holds
g . i c= f . i ) holds
product (f +* g) c= product f