theorem :: NDIFF10:13

for X, Y, Z being RealNormSpace
for f being PartFunc of [:X,Y:],Z
for U being Subset of [:X,Y:]
for I being LinearOperator of [:Y,X:],[:X,Y:] st U = dom f & f is_differentiable_on U & I is one-to-one & I is onto & I is isometric & ( 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
( partdiff`1 (f,u) = partdiff`2 ((f * I),v) & partdiff`2 (f,u) = partdiff`1 ((f * I),v) ) by Th11;