let X, Y, W be RealNormSpace; :: thesis:
let Z be Subset of [:X,Y:]; :: thesis:
let f be PartFunc of [:X,Y:],W; :: thesis:
assume AS: Z is open ; :: thesis:
set I = (IsoCPNrSP (X,Y)) " ;
set J = IsoCPNrSP (X,Y);
set g = f * ((IsoCPNrSP (X,Y)) ");
set E = ((IsoCPNrSP (X,Y)) ") " Z;
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;
((IsoCPNrSP (X,Y)) ") " Z = (IsoCPNrSP (X,Y)) .: Z by FUNCT_1:84;
then OP1: ((IsoCPNrSP (X,Y)) ") " Z is open by AS, LM025;
D1: dom <*X,Y*> = Seg (len <*X,Y*>) by FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44 ;
then D2: 1 in dom <*X,Y*> ;
then In (1,(dom <*X,Y*>)) = 1 by SUBSET_1:def 8;
then BX1: <*X,Y*> . (In (1,(dom <*X,Y*>))) = X ;
D3: 2 in dom <*X,Y*> by D1;
then In (2,(dom <*X,Y*>)) = 2 by SUBSET_1:def 8;
then BX2: <*X,Y*> . (In (2,(dom <*X,Y*>))) = Y ;
JE1: (IsoCPNrSP (X,Y)) " (((IsoCPNrSP (X,Y)) ") " Z) = ((IsoCPNrSP (X,Y)) ") .: (((IsoCPNrSP (X,Y)) ") " Z) by FUNCT_1:85
.= Z by X1, FUNCT_1:77 ;

hereby :: thesis:

assume P1: ( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z ) ; :: thesis:
P2: f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 by P1, LM300;
P3: f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 by P1, LM300;
P4: f `partial`1| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y)) by LM400, P1;
P5: f `partial`2| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (IsoCPNrSP (X,Y)) by LM401, P1;
for i being set st i in dom <*X,Y*> holds
( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,i & (f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),i) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z )

let i be set ; :: thesis:
assume CX: i in dom <*X,Y*> ; :: thesis:
then C1: ( i = 1 or i = 2 ) by D1, TARSKI:def 2, FINSEQ_1:2;
thus f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,i by CX, D1, P2, P3, TARSKI:def 2, FINSEQ_1:2; :: thesis:
thus (f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),i) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z by BX1, BX2, C1, P1, P4, P5, JE1, LM045; :: thesis:

end;

then GF1: ( f * ((IsoCPNrSP (X,Y)) ") is_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z & (f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z ) by NDIFF_5:57, OP1;
hence f is_differentiable_on Z by LM155; :: thesis:
hence f `| Z is_continuous_on Z by GF1, LMX1; :: thesis:

end;

assume X0: ( f is_differentiable_on Z & f `| Z is_continuous_on Z ) ; :: thesis:
then X1: f * ((IsoCPNrSP (X,Y)) ") is_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z by LM155;
X3: (f * ((IsoCPNrSP (X,Y)) ")) `| (((IsoCPNrSP (X,Y)) ") " Z) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z by X0, LMX1;
P2: f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 by D2, OP1, X1, X3, NDIFF_5:57;
hence f is_partial_differentiable_on`1 Z by LM300; :: thesis:
P3: f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 by D3, OP1, X1, X3, NDIFF_5:57;
hence f is_partial_differentiable_on`2 Z by LM300; :: thesis:
P6: (f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z by D2, OP1, X1, X3, NDIFF_5:57;
P7: (f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2) is_continuous_on ((IsoCPNrSP (X,Y)) ") " Z by D3, OP1, X1, X3, NDIFF_5:57;
f `partial`1| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),1)) * (IsoCPNrSP (X,Y)) by P2, LM300, LM400;
hence f `partial`1| Z is_continuous_on Z by BX1, P6, LM045, JE1; :: thesis:
f `partial`2| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (IsoCPNrSP (X,Y)) by P3, LM300, LM401;
hence f `partial`2| Z is_continuous_on Z by BX2, P7, LM045, JE1; :: thesis: