theorem Th24: :: TOPS_5:24

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 f) \ (dom g) holds
(proj (f,i)) .: (product (f +* g)) = f . i