let X, Y, W be RealNormSpace; for Z being Subset of [:X,Y:]
for r being Real
for f being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`2 Z holds
( r (#) f is_partial_differentiable_on`2 Z & (r (#) f) `partial`2| Z = r (#) (f `partial`2| Z) )
let Z be Subset of [:X,Y:]; for r being Real
for f being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`2 Z holds
( r (#) f is_partial_differentiable_on`2 Z & (r (#) f) `partial`2| Z = r (#) (f `partial`2| Z) )
let r be Real; for f being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`2 Z holds
( r (#) f is_partial_differentiable_on`2 Z & (r (#) f) `partial`2| Z = r (#) (f `partial`2| Z) )
let f be PartFunc of [:X,Y:],W; ( Z is open & f is_partial_differentiable_on`2 Z implies ( r (#) f is_partial_differentiable_on`2 Z & (r (#) f) `partial`2| Z = r (#) (f `partial`2| Z) ) )
assume that
O1:
Z is open
and
A1:
f is_partial_differentiable_on`2 Z
; ( r (#) f is_partial_differentiable_on`2 Z & (r (#) f) `partial`2| Z = r (#) (f `partial`2| Z) )
set h = r (#) f;
D1:
Z c= dom (r (#) f)
by A1, VFUNCT_1:def 4;
X1:
for x being Point of [:X,Y:] st x in Z holds
( r (#) f is_partial_differentiable_in`2 x & partdiff`2 ((r (#) f),x) = r * (partdiff`2 (f,x)) )
then
for x being Point of [:X,Y:] st x in Z holds
r (#) f is_partial_differentiable_in`2 x
;
hence P7:
r (#) f is_partial_differentiable_on`2 Z
by D1, O1, NDIFF5242; (r (#) f) `partial`2| Z = r (#) (f `partial`2| Z)
set fp = f `partial`2| Z;
P8:
( dom (f `partial`2| Z) = Z & ( for x being Point of [:X,Y:] st x in Z holds
(f `partial`2| Z) /. x = partdiff`2 (f,x) ) )
by A1, Def92;
P10:
dom (r (#) (f `partial`2| Z)) = Z
by P8, VFUNCT_1:def 4;
for x being Point of [:X,Y:] st x in Z holds
(r (#) (f `partial`2| Z)) /. x = partdiff`2 ((r (#) f),x)
proof
let x be
Point of
[:X,Y:];
( x in Z implies (r (#) (f `partial`2| Z)) /. x = partdiff`2 ((r (#) f),x) )
assume P11:
x in Z
;
(r (#) (f `partial`2| Z)) /. x = partdiff`2 ((r (#) f),x)
Z1:
(f `partial`2| Z) /. x = partdiff`2 (
f,
x)
by A1, P11, Def92;
thus (r (#) (f `partial`2| Z)) /. x =
r * ((f `partial`2| Z) /. x)
by P11, P10, VFUNCT_1:def 4
.=
partdiff`2 (
(r (#) f),
x)
by P11, X1, Z1
;
verum
end;
hence
(r (#) f) `partial`2| Z = r (#) (f `partial`2| Z)
by P7, P10, Def92; verum