theorem FX1: :: NDIFF_7:1

for X being set
for I, f being Function holds (f | X) * I = (f * I) | (I " X)