let G be RealNormSpace-Sequence; :: thesis: for F being RealNormSpace
for i being set
for f being PartFunc of (product G),F
for r being Real
for X being Subset of (product G) st X is open & i in dom G & f is_partial_differentiable_on X,i holds
( r (#) f is_partial_differentiable_on X,i & (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) )
let F be RealNormSpace; :: thesis: for i being set
for f being PartFunc of (product G),F
for r being Real
for X being Subset of (product G) st X is open & i in dom G & f is_partial_differentiable_on X,i holds
( r (#) f is_partial_differentiable_on X,i & (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) )
let i be set ; :: thesis: for f being PartFunc of (product G),F
for r being Real
for X being Subset of (product G) st X is open & i in dom G & f is_partial_differentiable_on X,i holds
( r (#) f is_partial_differentiable_on X,i & (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) )
let f be PartFunc of (product G),F; :: thesis: for r being Real
for X being Subset of (product G) st X is open & i in dom G & f is_partial_differentiable_on X,i holds
( r (#) f is_partial_differentiable_on X,i & (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) )
let r be Real; :: thesis: for X being Subset of (product G) st X is open & i in dom G & f is_partial_differentiable_on X,i holds
( r (#) f is_partial_differentiable_on X,i & (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) )
let X be Subset of (product G); :: thesis: ( X is open & i in dom G & f is_partial_differentiable_on X,i implies ( r (#) f is_partial_differentiable_on X,i & (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) ) )
assume that
O1: X is open and
A0: i in dom G and
A1: f is_partial_differentiable_on X,i ; :: thesis: ( r (#) f is_partial_differentiable_on X,i & (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) )
set h = r (#) f;
D1: X c= dom (r (#) f) by A1, VFUNCT_1:def 4;
X1: for x being Point of (product G) st x in X holds
( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )

proof

let x be Point of (product G); :: thesis: ( x in X implies ( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) ) )
assume x in X ; :: thesis: ( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )
then f is_partial_differentiable_in x,i by A1, O1, NDIFF_5:24;
hence ( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) ) by A0, NDIFF_5:30; :: thesis: verum

end;

then for x being Point of (product G) st x in X holds
r (#) f is_partial_differentiable_in x,i ;
hence P7: r (#) f is_partial_differentiable_on X,i by NDIFF_5:24, D1, O1; :: thesis: (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i))
set fp = f `partial| (X,i);
P8: ( dom (f `partial| (X,i)) = X & ( for x being Point of (product G) st x in X holds
(f `partial| (X,i)) /. x = partdiff (f,x,i) ) ) by A1, NDIFF_5:def 9;
P10: dom (r (#) (f `partial| (X,i))) = X by P8, VFUNCT_1:def 4;
for x being Point of (product G) st x in X holds
(r (#) (f `partial| (X,i))) /. x = partdiff ((r (#) f),x,i)

proof

let x be Point of (product G); :: thesis: ( x in X implies (r (#) (f `partial| (X,i))) /. x = partdiff ((r (#) f),x,i) )
assume P11: x in X ; :: thesis: (r (#) (f `partial| (X,i))) /. x = partdiff ((r (#) f),x,i)
thus (r (#) (f `partial| (X,i))) /. x = r * ((f `partial| (X,i)) /. x) by P11, P10, VFUNCT_1:def 4
.= r * (partdiff (f,x,i)) by A1, P11, NDIFF_5:def 9
.= partdiff ((r (#) f),x,i) by P11, X1 ; :: thesis: verum

end;

hence (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) by P7, P10, NDIFF_5:def 9; :: thesis: verum