let n, m be non empty Element of NAT ; :: thesis: for i being Element of NAT
for X being set
for f being PartFunc of (REAL-NS m),(REAL-NS n) st f is_partial_differentiable_on X,i holds
X is Subset of (REAL-NS m)
let i be Element of NAT ; :: thesis: for X being set
for f being PartFunc of (REAL-NS m),(REAL-NS n) st f is_partial_differentiable_on X,i holds
X is Subset of (REAL-NS m)
let X be set ; :: thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n) st f is_partial_differentiable_on X,i holds
X is Subset of (REAL-NS m)
let f be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: ( f is_partial_differentiable_on X,i implies X is Subset of (REAL-NS m) )
assume f is_partial_differentiable_on X,i ; :: thesis: X is Subset of (REAL-NS m)
then X c= dom f by Def19;
hence X is Subset of (REAL-NS m) by XBOOLE_1:1; :: thesis: verum