let W be RealNormSpace; :: thesis: for X, Y being RealNormSpace
for f being PartFunc of (product <*X,Y*>),W
for D being Subset of (product <*X,Y*>) st f is_differentiable_on D holds
for z being Point of (product <*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 (product <*X,Y*>),W
for D being Subset of (product <*X,Y*>) st f is_differentiable_on D holds
for z being Point of (product <*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 (product <*X,Y*>),W; :: thesis: for D being Subset of (product <*X,Y*>) st f is_differentiable_on D holds
for z being Point of (product <*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 (product <*X,Y*>); :: thesis: ( f is_differentiable_on D implies for z being Point of (product <*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 (product <*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) 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;
set J = (IsoCPNrSP (X,Y)) " ;
P1: ( dom (f `| D) = D & ( for x being Point of (product <*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 (product <*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 (product <*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 F1: 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 F2: (f `| D) . z = (f `| D) /. z by PARTFUN1:def 6
.= diff (f,z) by F1, P1 ;
F3: f is_differentiable_in z by F1, OP1, P1, AS2, NDIFF_1:31;
consider w being Point of [: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 ([:X,Y:],(product <*X,Y*>))) by LOPBAN_1:def 9;
F11: ((diff (f,z)) * I0) * (I0 ") = (modetrans ((diff (f,z)),(product <*X,Y*>),W)) * ((modetrans (I0,[:X,Y:],(product <*X,Y*>))) * (I0 ")) by RELAT_1:36
.= (modetrans ((diff (f,z)),(product <*X,Y*>),W)) * ((IsoCPNrSP (X,Y)) * ((IsoCPNrSP (X,Y)) ")) by LOPBAN_1:def 11
.= (modetrans ((diff (f,z)),(product <*X,Y*>),W)) * (id (rng I0)) by FUNCT_1:39
.= modetrans ((diff (f,z)),(product <*X,Y*>),W) by X1, FUNCT_2:17
.= (f `| D) . z by F2, LOPBAN_1:def 11 ;
w in (IsoCPNrSP (X,Y)) " D by F1, F4, P1, FUNCT_2:38;
then F12: (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. w) * (I0 ") = (diff ((f * (IsoCPNrSP (X,Y))),w)) * (I0 ") by P3, NDIFF_1:def 9;
F13: w = ((IsoCPNrSP (X,Y)) ") . z by F4, FUNCT_2:26;
thus (f `| D) . z = (((f * (IsoCPNrSP (X,Y))) `| ((IsoCPNrSP (X,Y)) " D)) /. (((IsoCPNrSP (X,Y)) ") . z)) * ((IsoCPNrSP (X,Y)) ") by F3, F4, F11, F12, F13, LM120; :: thesis: verum

end;

hence for z being Point of (product <*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