theorem Th8: :: NDIFF10:8

for X, Y being RealNormSpace
for Z being non empty set
for f being PartFunc of [:X,Y:],Z
for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y
for x being Point of X holds I . (y,x) = [x,y] ) holds
( dom (f * I) = I " (dom f) & ( for x being Point of X
for y being Point of Y holds (f * I) . (y,x) = f . (x,y) ) )