let m be non zero Element of NAT ; :: thesis: for i being Element of NAT
for X being Subset of (REAL m)
for r being Real
for f being PartFunc of (REAL m),REAL st X is open & 1 <= i & i <= m & 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)) & ( for x being Element of REAL m st x in X holds
((r (#) f) `partial| (X,i)) /. x = r * (partdiff (f,x,i)) ) )
let i be Element of NAT ; :: thesis: for X being Subset of (REAL m)
for r being Real
for f being PartFunc of (REAL m),REAL st X is open & 1 <= i & i <= m & 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)) & ( for x being Element of REAL m st x in X holds
((r (#) f) `partial| (X,i)) /. x = r * (partdiff (f,x,i)) ) )
let X be Subset of (REAL m); :: thesis: for r being Real
for f being PartFunc of (REAL m),REAL st X is open & 1 <= i & i <= m & 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)) & ( for x being Element of REAL m st x in X holds
((r (#) f) `partial| (X,i)) /. x = r * (partdiff (f,x,i)) ) )
let r be Real; :: thesis: for f being PartFunc of (REAL m),REAL st X is open & 1 <= i & i <= m & 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)) & ( for x being Element of REAL m st x in X holds
((r (#) f) `partial| (X,i)) /. x = r * (partdiff (f,x,i)) ) )
let f be PartFunc of (REAL m),REAL; :: thesis: ( X is open & 1 <= i & i <= m & 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)) & ( for x being Element of REAL m st x in X holds
((r (#) f) `partial| (X,i)) /. x = r * (partdiff (f,x,i)) ) ) )
assume A1: ( X is open & 1 <= i & i <= m & 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)) & ( for x being Element of REAL m st x in X holds
((r (#) f) `partial| (X,i)) /. x = r * (partdiff (f,x,i)) ) )
A2: dom (f `partial| (X,i)) = X by Def6, A1;
A3: X c= dom (r (#) f) by A1, VALUED_1:def 5;

A4: now :: thesis: for x being Element of REAL m st x in X holds
( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )

let x be Element of REAL m; :: 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, Th60;
hence ( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) ) by PDIFF_1:33; :: thesis: verum

end;

then A5: for x being Element of REAL m st x in X holds
r (#) f is_partial_differentiable_in x,i ;
then A6: r (#) f is_partial_differentiable_on X,i by A3, Th60, A1;
then A7: dom ((r (#) f) `partial| (X,i)) = X by Def6;

A8: now :: thesis: for x being Element of REAL m st x in X holds
((r (#) f) `partial| (X,i)) /. x = r * (partdiff (f,x,i))

let x be Element of REAL m; :: thesis: ( x in X implies ((r (#) f) `partial| (X,i)) /. x = r * (partdiff (f,x,i)) )
assume A9: x in X ; :: thesis: ((r (#) f) `partial| (X,i)) /. x = r * (partdiff (f,x,i))
then ((r (#) f) `partial| (X,i)) /. x = partdiff ((r (#) f),x,i) by A6, Def6;
hence ((r (#) f) `partial| (X,i)) /. x = r * (partdiff (f,x,i)) by A4, A9; :: thesis: verum

end;

dom (r (#) (f `partial| (X,i))) = dom (f `partial| (X,i)) by VALUED_1:def 5;
then A10: dom (r (#) (f `partial| (X,i))) = X by Def6, A1;

now :: thesis: for x being Element of REAL m st x in X holds
((r (#) f) `partial| (X,i)) . x = (r (#) (f `partial| (X,i))) . x

let x be Element of REAL m; :: thesis: ( x in X implies ((r (#) f) `partial| (X,i)) . x = (r (#) (f `partial| (X,i))) . x )
assume A11: x in X ; :: thesis: ((r (#) f) `partial| (X,i)) . x = (r (#) (f `partial| (X,i))) . x
hence ((r (#) f) `partial| (X,i)) . x = ((r (#) f) `partial| (X,i)) /. x by A7, PARTFUN1:def 6
.= r * (partdiff (f,x,i)) by A8, A11
.= r * ((f `partial| (X,i)) /. x) by A11, Def6, A1
.= r * ((f `partial| (X,i)) . x) by A11, A2, PARTFUN1:def 6
.= (r (#) (f `partial| (X,i))) . x by A11, A10, VALUED_1:def 5 ;
:: thesis: verum

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 A7, A10, A5, A8, A3, Th60, A1, PARTFUN1:5; :: thesis: verum