let X, Y, W be RealNormSpace; :: thesis: for Z being Subset of [:X,Y:]
for f being PartFunc of [:X,Y:],W holds
( ( f is_partial_differentiable_on`1 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 implies f is_partial_differentiable_on`1 Z ) & ( f is_partial_differentiable_on`2 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 implies f is_partial_differentiable_on`2 Z ) )
let Z be Subset of [:X,Y:]; :: thesis: for f being PartFunc of [:X,Y:],W holds
( ( f is_partial_differentiable_on`1 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 implies f is_partial_differentiable_on`1 Z ) & ( f is_partial_differentiable_on`2 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 implies f is_partial_differentiable_on`2 Z ) )
let f be PartFunc of [:X,Y:],W; :: thesis: ( ( f is_partial_differentiable_on`1 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 implies f is_partial_differentiable_on`1 Z ) & ( f is_partial_differentiable_on`2 Z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 implies f is_partial_differentiable_on`2 Z ) )
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;
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;
A1: dom (f * ((IsoCPNrSP (X,Y)) ")) = ((IsoCPNrSP (X,Y)) ") " (dom f) by RELAT_1:147;
A2: dom (IsoCPNrSP (X,Y)) = the carrier of [:X,Y:] by FUNCT_2:def 1;
thus ( f is_partial_differentiable_on`1 Z iff f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 ) :: thesis: ( f is_partial_differentiable_on`2 Z iff f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 )

proof

hereby :: thesis: ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 implies f is_partial_differentiable_on`1 Z )

assume P2: f is_partial_differentiable_on`1 Z ; :: thesis: f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1
for w being Point of (product <*X,Y*>) st w in ((IsoCPNrSP (X,Y)) ") " Z holds
(f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,1

proof

let w be Point of (product <*X,Y*>); :: thesis: ( w in ((IsoCPNrSP (X,Y)) ") " Z implies (f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,1 )
assume A4: w in ((IsoCPNrSP (X,Y)) ") " Z ; :: thesis: (f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,1
consider z being Point of [:X,Y:] such that
F4: w = (IsoCPNrSP (X,Y)) . z by X2, FUNCT_2:113;
((IsoCPNrSP (X,Y)) ") . w = z by A2, F4, FUNCT_1:34;
then z in Z by A4, FUNCT_2:38;
then (f | Z) * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 by P2, LM200;
hence (f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,1 by F4, FX1; :: thesis: verum

end;

hence f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 by A1, P2, RELAT_1:143; :: thesis: verum

end;

assume P2: f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,1 ; :: thesis: f is_partial_differentiable_on`1 Z
then P3: ((IsoCPNrSP (X,Y)) ") " Z c= ((IsoCPNrSP (X,Y)) ") " (dom f) by RELAT_1:147;
for z being Point of [:X,Y:] st z in Z holds
f | Z is_partial_differentiable_in`1 z

proof

let z be Point of [:X,Y:]; :: thesis: ( z in Z implies f | Z is_partial_differentiable_in`1 z )
assume A4: z in Z ; :: thesis: f | Z is_partial_differentiable_in`1 z
set w = (IsoCPNrSP (X,Y)) . z;
((IsoCPNrSP (X,Y)) ") . ((IsoCPNrSP (X,Y)) . z) = z by A2, FUNCT_1:34;
then F4: (IsoCPNrSP (X,Y)) . z in ((IsoCPNrSP (X,Y)) ") " Z by FUNCT_2:38, A4;
(f | Z) * ((IsoCPNrSP (X,Y)) ") = (f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) by FX1;
hence f | Z is_partial_differentiable_in`1 z by F4, P2, LM200; :: thesis: verum

end;

hence f is_partial_differentiable_on`1 Z by P3, X1, FUNCT_1:88; :: thesis: verum

end;

thus ( f is_partial_differentiable_on`2 Z iff f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 ) :: thesis: verum

proof

hereby :: thesis: ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 implies f is_partial_differentiable_on`2 Z )

assume P2: f is_partial_differentiable_on`2 Z ; :: thesis: f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2
for w being Point of (product <*X,Y*>) st w in ((IsoCPNrSP (X,Y)) ") " Z holds
(f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,2

proof

let w be Point of (product <*X,Y*>); :: thesis: ( w in ((IsoCPNrSP (X,Y)) ") " Z implies (f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,2 )
assume A4: w in ((IsoCPNrSP (X,Y)) ") " Z ; :: thesis: (f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,2
consider z being Point of [:X,Y:] such that
F4: w = (IsoCPNrSP (X,Y)) . z by X2, FUNCT_2:113;
F8: ((IsoCPNrSP (X,Y)) ") . w = z by A2, F4, FUNCT_1:34;
((IsoCPNrSP (X,Y)) ") . w in Z by FUNCT_2:38, A4;
then (f | Z) * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 by F8, P2, LM200;
hence (f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) is_partial_differentiable_in w,2 by F4, FX1; :: thesis: verum

end;

hence f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 by A1, P2, RELAT_1:143; :: thesis: verum

end;

assume P2: f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2 ; :: thesis: f is_partial_differentiable_on`2 Z
P3: ((IsoCPNrSP (X,Y)) ") " Z c= ((IsoCPNrSP (X,Y)) ") " (dom f) by P2, RELAT_1:147;
for z being Point of [:X,Y:] st z in Z holds
f | Z is_partial_differentiable_in`2 z

proof

let z be Point of [:X,Y:]; :: thesis: ( z in Z implies f | Z is_partial_differentiable_in`2 z )
assume A4: z in Z ; :: thesis: f | Z is_partial_differentiable_in`2 z
set w = (IsoCPNrSP (X,Y)) . z;
((IsoCPNrSP (X,Y)) ") . ((IsoCPNrSP (X,Y)) . z) = z by A2, FUNCT_1:34;
then F4: (IsoCPNrSP (X,Y)) . z in ((IsoCPNrSP (X,Y)) ") " Z by FUNCT_2:38, A4;
(f | Z) * ((IsoCPNrSP (X,Y)) ") = (f * ((IsoCPNrSP (X,Y)) ")) | (((IsoCPNrSP (X,Y)) ") " Z) by FX1;
hence f | Z is_partial_differentiable_in`2 z by F4, P2, LM200; :: thesis: verum

end;

hence f is_partial_differentiable_on`2 Z by P3, X1, FUNCT_1:88; :: thesis: verum

end;