let m, n be non zero Nat; :: thesis: for i being 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 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 ;
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:37;
hence r (#) f is_partial_differentiable_in x,i ; :: 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:37; :: thesis: verum