theorem Th26: :: HILB10_7:26

for x, y being object
for X being set
for f being Function holds (Ext (f,x,y)) | X = Ext ((f | X),x,y)