theorem Th11: :: NDIFF10:11

for X, Y, Z being RealNormSpace
for f being PartFunc of [:X,Y:],Z
for U being Subset of [:X,Y:]
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
for a being Point of X
for b being Point of Y
for u being Point of [:X,Y:]
for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds
( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )