let G be non-trivial RealNormSpace-Sequence; :: thesis: for F being non trivial RealNormSpace
for f being PartFunc of (product G),F
for X, i being set st i in dom G & f is_partial_differentiable_on X,i holds
X is Subset of (product G)
let F be non trivial RealNormSpace; :: thesis: for f being PartFunc of (product G),F
for X, i being set st i in dom G & f is_partial_differentiable_on X,i holds
X is Subset of (product G)
let f be PartFunc of (product G),F; :: thesis: for X, i being set st i in dom G & f is_partial_differentiable_on X,i holds
X is Subset of (product G)
let X, i be set ; :: thesis: ( i in dom G & f is_partial_differentiable_on X,i implies X is Subset of (product G) )
assume ( i in dom G & f is_partial_differentiable_on X,i ) ; :: thesis: X is Subset of (product G)
then X c= dom f by Def19;
hence X is Subset of (product G) by XBOOLE_1:1; :: thesis: verum