let S be RealNormSpace-Sequence; :: thesis: for T being RealNormSpace
for Z being Subset of (product S)
for f being PartFunc of (product S),T
for i being set st Z is open & f is_differentiable_on Z holds
( f is_partial_differentiable_on Z,i & ( for x being Point of (product S) st x in Z holds
(f `partial| (Z,i)) /. x = ((f `| Z) /. x) * (reproj ((In (i,(dom S))),(0. (product S)))) ) )
let T be RealNormSpace; :: thesis: for Z being Subset of (product S)
for f being PartFunc of (product S),T
for i being set st Z is open & f is_differentiable_on Z holds
( f is_partial_differentiable_on Z,i & ( for x being Point of (product S) st x in Z holds
(f `partial| (Z,i)) /. x = ((f `| Z) /. x) * (reproj ((In (i,(dom S))),(0. (product S)))) ) )
let Z be Subset of (product S); :: thesis: for f being PartFunc of (product S),T
for i being set st Z is open & f is_differentiable_on Z holds
( f is_partial_differentiable_on Z,i & ( for x being Point of (product S) st x in Z holds
(f `partial| (Z,i)) /. x = ((f `| Z) /. x) * (reproj ((In (i,(dom S))),(0. (product S)))) ) )
let f be PartFunc of (product S),T; :: thesis: for i being set st Z is open & f is_differentiable_on Z holds
( f is_partial_differentiable_on Z,i & ( for x being Point of (product S) st x in Z holds
(f `partial| (Z,i)) /. x = ((f `| Z) /. x) * (reproj ((In (i,(dom S))),(0. (product S)))) ) )
let i be set ; :: thesis: ( Z is open & f is_differentiable_on Z implies ( f is_partial_differentiable_on Z,i & ( for x being Point of (product S) st x in Z holds
(f `partial| (Z,i)) /. x = ((f `| Z) /. x) * (reproj ((In (i,(dom S))),(0. (product S)))) ) ) )
assume that
A1: Z is open and
A2: f is_differentiable_on Z ; :: thesis: ( f is_partial_differentiable_on Z,i & ( for x being Point of (product S) st x in Z holds
(f `partial| (Z,i)) /. x = ((f `| Z) /. x) * (reproj ((In (i,(dom S))),(0. (product S)))) ) )
A4: for x being Point of (product S) st x in Z holds
( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom S))),(0. (product S)))) )

proof

let x be Point of (product S); :: thesis: ( x in Z implies ( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom S))),(0. (product S)))) ) )
assume x in Z ; :: thesis: ( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom S))),(0. (product S)))) )
then f is_differentiable_in x by A1, A2, NDIFF_1:31;
hence ( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom S))),(0. (product S)))) ) by NDIFF_5:41; :: thesis: verum

end;

then for x being Point of (product S) st x in Z holds
f is_partial_differentiable_in x,i ;
hence A5: f is_partial_differentiable_on Z,i by A1, A2, NDIFF_5:24; :: thesis: for x being Point of (product S) st x in Z holds
(f `partial| (Z,i)) /. x = ((f `| Z) /. x) * (reproj ((In (i,(dom S))),(0. (product S))))
let x be Point of (product S); :: thesis: ( x in Z implies (f `partial| (Z,i)) /. x = ((f `| Z) /. x) * (reproj ((In (i,(dom S))),(0. (product S)))) )
assume A6: x in Z ; :: thesis: (f `partial| (Z,i)) /. x = ((f `| Z) /. x) * (reproj ((In (i,(dom S))),(0. (product S))))
hence (f `partial| (Z,i)) /. x = partdiff (f,x,i) by A5, NDIFF_5:def 9
.= (diff (f,x)) * (reproj ((In (i,(dom S))),(0. (product S)))) by A4, A6
.= ((f `| Z) /. x) * (reproj ((In (i,(dom S))),(0. (product S)))) by A2, A6, NDIFF_1:def 9 ;
:: thesis: verum