theorem Th25: :: HILB10_7:25

for x, y being object
for f, g being Function holds (Ext (f,x,y)) * g = Ext ((f * g),x,y)