theorem Th35: :: HILB10_7:35

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)*>