let n, m be non empty Element of NAT ; :: thesis: for i being Element of NAT
for r being Real
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds
( r (#) f is_partial_differentiable_in x,i & partdiff (r (#) f),x,i = r * (partdiff f,x,i) )
let i be Element of NAT ; :: thesis: for r being Real
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds
( r (#) f is_partial_differentiable_in x,i & partdiff (r (#) f),x,i = r * (partdiff f,x,i) )
let r be Real; :: thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds
( r (#) f is_partial_differentiable_in x,i & partdiff (r (#) f),x,i = r * (partdiff f,x,i) )
let f be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for x being Point of (REAL-NS m) st f is_partial_differentiable_in x,i holds
( r (#) f is_partial_differentiable_in x,i & partdiff (r (#) f),x,i = r * (partdiff f,x,i) )
let x be Point of (REAL-NS m); :: thesis: ( f is_partial_differentiable_in x,i implies ( r (#) f is_partial_differentiable_in x,i & partdiff (r (#) f),x,i = r * (partdiff f,x,i) ) )
assume f is_partial_differentiable_in x,i ; :: thesis: ( r (#) f is_partial_differentiable_in x,i & partdiff (r (#) f),x,i = r * (partdiff f,x,i) )
then A1: f * (reproj i,x) is_differentiable_in (Proj i,m) . x by Def9;
r (#) (f * (reproj i,x)) = (r (#) f) * (reproj i,x) by Th27;
then (r (#) f) * (reproj i,x) is_differentiable_in (Proj i,m) . x by A1, NDIFF_1:42;
hence r (#) f is_partial_differentiable_in x,i by Def9; :: thesis: partdiff (r (#) f),x,i = r * (partdiff f,x,i)
diff (r (#) (f * (reproj i,x))),((Proj i,m) . x) = partdiff (r (#) f),x,i by Th27;
hence partdiff (r (#) f),x,i = r * (partdiff f,x,i) by A1, NDIFF_1:42; :: thesis: verum