let W be RealNormSpace; :: thesis: for X, Y being RealNormSpace
for f being PartFunc of [:X,Y:],W
for D being Subset of [:X,Y:] st f is_differentiable_on D holds
for z being Point of [:X,Y:] st z in dom (f `| D) holds
(f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ")
let X, Y be RealNormSpace; :: thesis: for f being PartFunc of [:X,Y:],W
for D being Subset of [:X,Y:] st f is_differentiable_on D holds
for z being Point of [:X,Y:] st z in dom (f `| D) holds
(f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ")
let f be PartFunc of [:X,Y:],W; :: thesis: for D being Subset of [:X,Y:] st f is_differentiable_on D holds
for z being Point of [:X,Y:] st z in dom (f `| D) holds
(f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ")
let D be Subset of [:X,Y:]; :: thesis: ( f is_differentiable_on D implies for z being Point of [:X,Y:] st z in dom (f `| D) holds
(f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ") )
assume AS2: f is_differentiable_on D ; :: thesis: for z being Point of [:X,Y:] st z in dom (f `| D) holds
(f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ")
then OP1: D is open by NDIFF_1:32;
set I = (IsoCPNrSP (X,Y)) " ;
X1: ( (IsoCPNrSP (X,Y)) " = (IsoCPNrSP (X,Y)) " & (IsoCPNrSP (X,Y)) " is one-to-one & (IsoCPNrSP (X,Y)) " is onto & ( for x being Point of X
for y being Point of Y holds ((IsoCPNrSP (X,Y)) ") . <*x,y*> = [x,y] ) & 0. [:X,Y:] = ((IsoCPNrSP (X,Y)) ") . (0. (product <*X,Y*>)) & (IsoCPNrSP (X,Y)) " is isometric ) by defISOA1, defISOA2;
set J = IsoCPNrSP (X,Y);
X2: ( IsoCPNrSP (X,Y) is one-to-one & IsoCPNrSP (X,Y) is onto & ( for x being Point of X
for y being Point of Y holds (IsoCPNrSP (X,Y)) . (x,y) = <*x,y*> ) & 0. (product <*X,Y*>) = (IsoCPNrSP (X,Y)) . (0. [:X,Y:]) & IsoCPNrSP (X,Y) is isometric ) by defISO, ZeZe;
P1: ( dom (f `| D) = D & ( for x being Point of [:X,Y:] st x in D holds
(f `| D) /. x = diff (f,x) ) ) by NDIFF_1:def 9, AS2;
set g = f * ((IsoCPNrSP (X,Y)) ");
set E = ((IsoCPNrSP (X,Y)) ") " D;
P3: f * ((IsoCPNrSP (X,Y)) ") is_differentiable_on ((IsoCPNrSP (X,Y)) ") " D by LM155, AS2;
for z being Point of [:X,Y:] st z in dom (f `| D) holds
(f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ")

proof

let z be Point of [:X,Y:]; :: thesis: ( z in dom (f `| D) implies (f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ") )
assume F1X: z in dom (f `| D) ; :: thesis: (f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ")
then F1: z in D by AS2, NDIFF_1:def 9;
F2: (f `| D) . z = (f `| D) /. z by F1X, PARTFUN1:def 6
.= diff (f,z) by F1X, P1 ;
F3: f is_differentiable_in z by F1, OP1, AS2, NDIFF_1:31;
consider w being Point of (product <*X,Y*>) such that
F4: z = ((IsoCPNrSP (X,Y)) ") . w by X1, FUNCT_2:113;
reconsider I0 = (IsoCPNrSP (X,Y)) " as Point of (R_NormSpace_of_BoundedLinearOperators ((product <*X,Y*>),[:X,Y:])) by LOPBAN_1:def 9;
F9: ((diff (f,z)) * I0) * (I0 ") = (diff ((f * ((IsoCPNrSP (X,Y)) ")),w)) * (I0 ") by F3, F4, LM120;
F11: ((diff (f,z)) * I0) * (I0 ") = (modetrans ((diff (f,z)),[:X,Y:],W)) * ((modetrans (I0,(product <*X,Y*>),[:X,Y:])) * (I0 ")) by RELAT_1:36
.= (modetrans ((diff (f,z)),[:X,Y:],W)) * (((IsoCPNrSP (X,Y)) ") * (((IsoCPNrSP (X,Y)) ") ")) by LOPBAN_1:def 11
.= (modetrans ((diff (f,z)),[:X,Y:],W)) * (id (rng I0)) by FUNCT_1:39
.= modetrans ((diff (f,z)),[:X,Y:],W) by X1, FUNCT_2:17
.= (f `| D) . z by F2, LOPBAN_1:def 11 ;
w in ((IsoCPNrSP (X,Y)) ") " D by F4, F1, FUNCT_2:38;
then (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. w) * (I0 ") = (diff ((f * ((IsoCPNrSP (X,Y)) ")),w)) * (I0 ") by P3, NDIFF_1:def 9;
hence (f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ") by F4, F9, F11, X2, FUNCT_1:35; :: thesis: verum

end;

hence for z being Point of [:X,Y:] st z in dom (f `| D) holds
(f `| D) . z = (((f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " D)) /. ((IsoCPNrSP (X,Y)) . z)) * (((IsoCPNrSP (X,Y)) ") ") ; :: thesis: verum