let X, Y, W be RealNormSpace; :: thesis: for Z being Subset of [:X,Y:]
for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`1 Z holds
f `partial`1| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y))
let Z be Subset of [:X,Y:]; :: thesis: for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`1 Z holds
f `partial`1| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y))
let f be PartFunc of [:X,Y:],W; :: thesis: ( f is_partial_differentiable_on`1 Z implies f `partial`1| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y)) )
assume AS0: f is_partial_differentiable_on`1 Z ; :: thesis: f `partial`1| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y))
set I = (IsoCPNrSP (X,Y)) " ;
set J = IsoCPNrSP (X,Y);
set g = f * ((IsoCPNrSP (X,Y)) ");
set E = ((IsoCPNrSP (X,Y)) ") " Z;
A2: dom (IsoCPNrSP (X,Y)) = the carrier of [:X,Y:] by FUNCT_2:def 1;
set fpz = f `partial`1| Z;
P1: ( dom (f `partial`1| Z) = Z & ( for z being Point of [:X,Y:] st z in Z holds
(f `partial`1| Z) /. z = partdiff`1 (f,z) ) ) by Def91, AS0;
set gpe = (f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1);
P3X: f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 by LM300, AS0;
then P3: ( dom ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) = ((IsoCPNrSP (X,Y)) ") " Z & ( for x being Point of (product <*X,Y*>) st x in ((IsoCPNrSP (X,Y)) ") " Z holds
((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) /. x = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),x,1) ) ) by NDIFF_5:def 9;
P4: dom (((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y))) = (IsoCPNrSP (X,Y)) " (((IsoCPNrSP (X,Y)) ") " Z) by P3, RELAT_1:147
.= (IsoCPNrSP (X,Y)) " ((IsoCPNrSP (X,Y)) .: Z) by FUNCT_1:84
.= Z by A2, FUNCT_1:94 ;

now :: thesis: for x being object st x in dom (f `partial`1| Z) holds
(f `partial`1| Z) . x = (((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y))) . x

let x be object ; :: thesis: ( x in dom (f `partial`1| Z) implies (f `partial`1| Z) . x = (((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y))) . x )
assume P40: x in dom (f `partial`1| Z) ; :: thesis: (f `partial`1| Z) . x = (((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y))) . x
then reconsider z = x as Point of [:X,Y:] ;
P44: (IsoCPNrSP (X,Y)) . z in (IsoCPNrSP (X,Y)) .: Z by P1, P40, FUNCT_2:35;
((IsoCPNrSP (X,Y)) ") " = IsoCPNrSP (X,Y) by FUNCT_1:43;
then P42: (IsoCPNrSP (X,Y)) . z in ((IsoCPNrSP (X,Y)) ") " Z by P44, FUNCT_1:85;
thus (f `partial`1| Z) . x = (f `partial`1| Z) /. z by PARTFUN1:def 6, P40
.= partdiff`1 (f,z) by P1, P40
.= partdiff ((f * ((IsoCPNrSP (X,Y)) ")),((IsoCPNrSP (X,Y)) . z),1) by LM210
.= ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) /. ((IsoCPNrSP (X,Y)) . z) by P3X, P42, NDIFF_5:def 9
.= ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) . ((IsoCPNrSP (X,Y)) . z) by P42, PARTFUN1:def 6, P3
.= (((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y))) . x by A2, FUNCT_1:13 ; :: thesis: verum

end;

hence f `partial`1| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y)) by P1, P4, FUNCT_1:2; :: thesis: verum