let G be RealNormSpace-Sequence; for F being RealNormSpace
for i being set
for f being PartFunc of (product G),F
for r being Real
for X being Subset of (product G) st X is open & i in dom G & 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)) )
let F be RealNormSpace; for i being set
for f being PartFunc of (product G),F
for r being Real
for X being Subset of (product G) st X is open & i in dom G & 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)) )
let i be set ; for f being PartFunc of (product G),F
for r being Real
for X being Subset of (product G) st X is open & i in dom G & 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)) )
let f be PartFunc of (product G),F; for r being Real
for X being Subset of (product G) st X is open & i in dom G & 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)) )
let r be Real; for X being Subset of (product G) st X is open & i in dom G & 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)) )
let X be Subset of (product G); ( X is open & i in dom G & 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)) ) )
assume that
O1:
X is open
and
A0:
i in dom G
and
A1:
f is_partial_differentiable_on X,i
; ( r (#) f is_partial_differentiable_on X,i & (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) )
set h = r (#) f;
D1:
X c= dom (r (#) f)
by A1, VFUNCT_1:def 4;
X1:
for x being Point of (product G) st x in X holds
( r (#) f is_partial_differentiable_in x,i & partdiff ((r (#) f),x,i) = r * (partdiff (f,x,i)) )
proof
let x be
Point of
(product G);
( 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
;
( 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, O1, NDIFF_5:24;
hence
(
r (#) f is_partial_differentiable_in x,
i &
partdiff (
(r (#) f),
x,
i)
= r * (partdiff (f,x,i)) )
by A0, NDIFF_5:30;
verum
end;
then
for x being Point of (product G) st x in X holds
r (#) f is_partial_differentiable_in x,i
;
hence P7:
r (#) f is_partial_differentiable_on X,i
by NDIFF_5:24, D1, O1; (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i))
set fp = f `partial| (X,i);
P8:
( dom (f `partial| (X,i)) = X & ( for x being Point of (product G) st x in X holds
(f `partial| (X,i)) /. x = partdiff (f,x,i) ) )
by A1, NDIFF_5:def 9;
P10:
dom (r (#) (f `partial| (X,i))) = X
by P8, VFUNCT_1:def 4;
for x being Point of (product G) st x in X holds
(r (#) (f `partial| (X,i))) /. x = partdiff ((r (#) f),x,i)
proof
let x be
Point of
(product G);
( x in X implies (r (#) (f `partial| (X,i))) /. x = partdiff ((r (#) f),x,i) )
assume P11:
x in X
;
(r (#) (f `partial| (X,i))) /. x = partdiff ((r (#) f),x,i)
thus (r (#) (f `partial| (X,i))) /. x =
r * ((f `partial| (X,i)) /. x)
by P11, P10, VFUNCT_1:def 4
.=
r * (partdiff (f,x,i))
by A1, P11, NDIFF_5:def 9
.=
partdiff (
(r (#) f),
x,
i)
by P11, X1
;
verum
end;
hence
(r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i))
by P7, P10, NDIFF_5:def 9; verum