theorem Th25: :: TOPS_5:25

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
for i being object st i in dom g holds
(proj (f,i)) .: (product (f +* g)) = g . i