theorem Th7: :: TOPALG_4:7

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