theorem Th26: :: TOPS_5:26

for f, g being non-empty Function st dom g = 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 g) = g . i