theorem Th37: :: HILB10_7:37

for x, y, z being object
for f being Function st z in dom f holds
Ext ({(f . z)},x,y) = {((Ext (f,x,y)) . z)}