let r be Real; :: thesis: for G being non-trivial RealNormSpace-Sequence
for F being non trivial RealNormSpace
for f being PartFunc of (product G),F
for x being Point of (product G)
for i being set st i in dom G & 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 G be non-trivial RealNormSpace-Sequence; :: thesis: for F being non trivial RealNormSpace
for f being PartFunc of (product G),F
for x being Point of (product G)
for i being set st i in dom G & 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 non trivial RealNormSpace; :: thesis: for f being PartFunc of (product G),F
for x being Point of (product G)
for i being set st i in dom G & 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 (product G),F; :: thesis: for x being Point of (product G)
for i being set st i in dom G & 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 (product G); :: thesis: for i being set st i in dom G & 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 i0 be set ; :: thesis: ( i0 in dom G & f is_partial_differentiable_in x,i0 implies ( r (#) f is_partial_differentiable_in x,i0 & partdiff ((r (#) f),x,i0) = r * (partdiff (f,x,i0)) ) )
assume AS: i0 in dom G ; :: thesis: ( not f is_partial_differentiable_in x,i0 or ( r (#) f is_partial_differentiable_in x,i0 & partdiff ((r (#) f),x,i0) = r * (partdiff (f,x,i0)) ) )
set i = modetrans (G,i0);
assume f is_partial_differentiable_in x,i0 ; :: thesis: ( r (#) f is_partial_differentiable_in x,i0 & partdiff ((r (#) f),x,i0) = r * (partdiff (f,x,i0)) )
then A1: f * (reproj ((modetrans (G,i0)),x)) is_differentiable_in (proj (modetrans (G,i0))) . x by Def9;
r (#) (f * (reproj ((modetrans (G,i0)),x))) = (r (#) f) * (reproj ((modetrans (G,i0)),x)) by AS, Th27;
then (r (#) f) * (reproj ((modetrans (G,i0)),x)) is_differentiable_in (proj (modetrans (G,i0))) . x by A1, NDIFF_1:37;
hence r (#) f is_partial_differentiable_in x,i0 by Def9; :: thesis: partdiff ((r (#) f),x,i0) = r * (partdiff (f,x,i0))
thus partdiff ((r (#) f),x,i0) = diff ((r (#) (f * (reproj ((modetrans (G,i0)),x)))),((proj (modetrans (G,i0))) . x)) by AS, Th27
.= r * (partdiff (f,x,i0)) by A1, NDIFF_1:37 ; :: thesis: verum