let m be non empty Element of NAT ; :: thesis:
let i be Element of NAT ; :: thesis:
let X be Subset of (REAL m); :: thesis:
let r be Real; :: thesis:
let f be PartFunc of (REAL m),REAL; :: thesis:
assume AS: ( X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i ) ; :: thesis:
Q1: dom (f `partial| (X,i)) = X by DefPDX, AS;
dom (r (#) f) = dom f by VALUED_1:def 5;
then P3: X c= dom (r (#) f) by AS, PDIFF734;

XX1: now :: thesis:

let x be Element of REAL m; :: thesis:
assume x in X ; :: thesis:
then f is_partial_differentiable_in x,i by AS, PDIFF734;
hence ( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) ) by PDIFF_1:33; :: thesis:

end;

then P7: for x being Element of REAL m st x in X holds
r (#) f is_partial_differentiable_in x,i ;
then P8: r (#) f is_partial_differentiable_on X,i by P3, PDIFF734, AS;
then P9: dom ((r (#) f) `partial| (X,i)) = X by DefPDX;

P10: now :: thesis:

let x be Element of REAL m; :: thesis:
assume P10: x in X ; :: thesis:
then ((r (#) f) `partial| (X,i)) /. x = partdiff ((r (#) f),x,i) by P8, DefPDX;
hence ((r (#) f) `partial| (X,i)) /. x = r * (partdiff (f,x,i)) by XX1, P10; :: thesis:

end;

dom (r (#) (f `partial| (X,i))) = dom (f `partial| (X,i)) by VALUED_1:def 5;
then P11: dom (r (#) (f `partial| (X,i))) = X by DefPDX, AS;

let x be Element of REAL m; :: thesis:
assume A1: x in X ; :: thesis:
thus ((r (#) f) `partial| (X,i)) . x = ((r (#) f) `partial| (X,i)) /. x by A1, P9, PARTFUN1:def 6
.= r * (partdiff (f,x,i)) by P10, A1
.= r * ((f `partial| (X,i)) /. x) by A1, DefPDX, AS
.= r * ((f `partial| (X,i)) . x) by A1, Q1, PARTFUN1:def 6
.= (r (#) (f `partial| (X,i))) . x by A1, P11, VALUED_1:def 5 ; :: thesis:

end;

hence ( r (#) f is_partial_differentiable_on X,i & (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) & ( for x being Element of REAL m st x in X holds
((r (#) f) `partial| (X,i)) /. x = r * (partdiff (f,x,i)) ) ) by P9, P11, P7, P10, P3, PDIFF734, AS, PARTFUN1:5; :: thesis: