theorem Th8: :: TOPALG_4:8

for f, g being Function st dom f = dom g holds
pr2 <:f,g:> = g