theorem
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
( (
f is_partial_differentiable_in`1 u implies
f * I is_partial_differentiable_in`2 v ) & (
f * I is_partial_differentiable_in`2 v implies
f is_partial_differentiable_in`1 u ) & (
f is_partial_differentiable_in`2 u implies
f * I is_partial_differentiable_in`1 v ) & (
f * I is_partial_differentiable_in`1 v implies
f is_partial_differentiable_in`2 u ) )
by Th11;