let X, Y, W be RealNormSpace; for Z being Subset of [:X,Y:]
for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`2 Z holds
f `partial`2| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (IsoCPNrSP (X,Y))
let Z be Subset of [:X,Y:]; for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_on`2 Z holds
f `partial`2| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (IsoCPNrSP (X,Y))
let f be PartFunc of [:X,Y:],W; ( f is_partial_differentiable_on`2 Z implies f `partial`2| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (IsoCPNrSP (X,Y)) )
assume AS0:
f is_partial_differentiable_on`2 Z
; f `partial`2| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (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`2| Z;
P1:
( dom (f `partial`2| Z) = Z & ( for z being Point of [:X,Y:] st z in Z holds
(f `partial`2| Z) /. z = partdiff`2 (f,z) ) )
by Def92, AS0;
set gpe = (f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2);
P3X:
f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_on ((IsoCPNrSP (X,Y)) ") " Z,2
by LM300, AS0;
then P3:
( dom ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) = ((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),2)) /. x = partdiff ((f * ((IsoCPNrSP (X,Y)) ")),x,2) ) )
by NDIFF_5:def 9;
P4: dom (((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (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 for x being object st x in dom (f `partial`2| Z) holds
(f `partial`2| Z) . x = (((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (IsoCPNrSP (X,Y))) . xlet x be
object ;
( x in dom (f `partial`2| Z) implies (f `partial`2| Z) . x = (((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (IsoCPNrSP (X,Y))) . x )assume P40:
x in dom (f `partial`2| Z)
;
(f `partial`2| Z) . x = (((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (IsoCPNrSP (X,Y))) . xthen 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`2| Z) . x =
(f `partial`2| Z) /. z
by PARTFUN1:def 6, P40
.=
partdiff`2 (
f,
z)
by P1, P40
.=
partdiff (
(f * ((IsoCPNrSP (X,Y)) ")),
((IsoCPNrSP (X,Y)) . z),2)
by LM210
.=
((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) /. ((IsoCPNrSP (X,Y)) . z)
by P3X, P42, NDIFF_5:def 9
.=
((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) . ((IsoCPNrSP (X,Y)) . z)
by P3, P42, PARTFUN1:def 6
.=
(((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (IsoCPNrSP (X,Y))) . x
by A2, FUNCT_1:13
;
verum end;
hence
f `partial`2| Z = ((f * ((IsoCPNrSP (X,Y)) ")) `partial| ((((IsoCPNrSP (X,Y)) ") " Z),2)) * (IsoCPNrSP (X,Y))
by P1, P4, FUNCT_1:2; verum