let m be non zero Element of NAT ; :: thesis: for X being Subset of (REAL m)
for r being Real
for I being non empty FinSequence of NAT
for f being PartFunc of (REAL m),REAL st X is open & rng I c= Seg 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)) )
let Z be Subset of (REAL m); :: thesis: for r being Real
for I being non empty FinSequence of NAT
for f being PartFunc of (REAL m),REAL st Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I holds
( r (#) f is_partial_differentiable_on Z,I & (r (#) f) `partial| (Z,I) = r (#) (f `partial| (Z,I)) )
let r be Real; :: thesis: for I being non empty FinSequence of NAT
for f being PartFunc of (REAL m),REAL st Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I holds
( r (#) f is_partial_differentiable_on Z,I & (r (#) f) `partial| (Z,I) = r (#) (f `partial| (Z,I)) )
let I be non empty FinSequence of NAT ; :: thesis: for f being PartFunc of (REAL m),REAL st Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I holds
( r (#) f is_partial_differentiable_on Z,I & (r (#) f) `partial| (Z,I) = r (#) (f `partial| (Z,I)) )
let f be PartFunc of (REAL m),REAL; :: thesis: ( Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I implies ( r (#) f is_partial_differentiable_on Z,I & (r (#) f) `partial| (Z,I) = r (#) (f `partial| (Z,I)) ) )
assume A1: ( Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I ) ; :: thesis: ( r (#) f is_partial_differentiable_on Z,I & (r (#) f) `partial| (Z,I) = r (#) (f `partial| (Z,I)) )
hence r (#) f is_partial_differentiable_on Z,I by Th78; :: thesis: (r (#) f) `partial| (Z,I) = r (#) (f `partial| (Z,I))
reconsider k = (len I) - 1 as Element of NAT by INT_1:5, FINSEQ_1:20;
A2: (PartDiffSeq (f,Z,I)) . k is_partial_differentiable_on Z,I /. (k + 1) by A1;
1 <= k + 1 by NAT_1:11;
then I /. (k + 1) in Seg m by A1, Lm6;
then A3: ( 1 <= I /. (k + 1) & I /. (k + 1) <= m ) by FINSEQ_1:1;
(PartDiffSeq ((r (#) f),Z,I)) . (k + 1) = ((PartDiffSeq ((r (#) f),Z,I)) . k) `partial| (Z,(I /. (k + 1))) by Def7
.= (r (#) ((PartDiffSeq (f,Z,I)) . k)) `partial| (Z,(I /. (k + 1))) by A1, Th78
.= r (#) (((PartDiffSeq (f,Z,I)) . k) `partial| (Z,(I /. (k + 1)))) by A2, A1, A3, Th67 ;
hence (r (#) f) `partial| (Z,I) = r (#) (f `partial| (Z,I)) by Def7; :: thesis: verum