let X, Y, W be RealNormSpace; :: thesis: 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`1 Z holds
( r (#) f is_partial_differentiable_on`1 Z & (r (#) f) `partial`1| Z = r (#) (f `partial`1| Z) )
let Z be Subset of [:X,Y:]; :: thesis: for r being Real
for f being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`1 Z holds
( r (#) f is_partial_differentiable_on`1 Z & (r (#) f) `partial`1| Z = r (#) (f `partial`1| Z) )
let r be Real; :: thesis: for f being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`1 Z holds
( r (#) f is_partial_differentiable_on`1 Z & (r (#) f) `partial`1| Z = r (#) (f `partial`1| Z) )
let f be PartFunc of [:X,Y:],W; :: thesis: ( Z is open & f is_partial_differentiable_on`1 Z implies ( r (#) f is_partial_differentiable_on`1 Z & (r (#) f) `partial`1| Z = r (#) (f `partial`1| Z) ) )
assume that
O1: Z is open and
A1: f is_partial_differentiable_on`1 Z ; :: thesis: ( r (#) f is_partial_differentiable_on`1 Z & (r (#) f) `partial`1| Z = r (#) (f `partial`1| 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`1 x & partdiff`1 ((r (#) f),x) = r * (partdiff`1 (f,x)) )

proof

let x be Point of [:X,Y:]; :: thesis: ( x in Z implies ( r (#) f is_partial_differentiable_in`1 x & partdiff`1 ((r (#) f),x) = r * (partdiff`1 (f,x)) ) )
assume x in Z ; :: thesis: ( r (#) f is_partial_differentiable_in`1 x & partdiff`1 ((r (#) f),x) = r * (partdiff`1 (f,x)) )
then f is_partial_differentiable_in`1 x by A1, O1, NDIFF5241;
hence ( r (#) f is_partial_differentiable_in`1 x & partdiff`1 ((r (#) f),x) = r * (partdiff`1 (f,x)) ) by LM217; :: thesis: verum

end;

then for x being Point of [:X,Y:] st x in Z holds
r (#) f is_partial_differentiable_in`1 x ;
hence P7: r (#) f is_partial_differentiable_on`1 Z by D1, O1, NDIFF5241; :: thesis: (r (#) f) `partial`1| Z = r (#) (f `partial`1| Z)
set fp = f `partial`1| Z;
P8: ( dom (f `partial`1| Z) = Z & ( for x being Point of [:X,Y:] st x in Z holds
(f `partial`1| Z) /. x = partdiff`1 (f,x) ) ) by A1, Def91;
P10: dom (r (#) (f `partial`1| Z)) = Z by P8, VFUNCT_1:def 4;
for x being Point of [:X,Y:] st x in Z holds
(r (#) (f `partial`1| Z)) /. x = partdiff`1 ((r (#) f),x)

proof

let x be Point of [:X,Y:]; :: thesis: ( x in Z implies (r (#) (f `partial`1| Z)) /. x = partdiff`1 ((r (#) f),x) )
assume P11: x in Z ; :: thesis: (r (#) (f `partial`1| Z)) /. x = partdiff`1 ((r (#) f),x)
Z1: (f `partial`1| Z) /. x = partdiff`1 (f,x) by A1, P11, Def91;
thus (r (#) (f `partial`1| Z)) /. x = r * ((f `partial`1| Z) /. x) by P11, P10, VFUNCT_1:def 4
.= partdiff`1 ((r (#) f),x) by P11, X1, Z1 ; :: thesis: verum

end;

hence (r (#) f) `partial`1| Z = r (#) (f `partial`1| Z) by P7, P10, Def91; :: thesis: verum