let m be non empty Element of NAT ; :: thesis: for i being Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for r being Real st X is open & f is_partial_differentiable_up_to_order i,X holds
r (#) f is_partial_differentiable_up_to_order i,X
let i be Element of NAT ; :: thesis: for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for r being Real st X is open & f is_partial_differentiable_up_to_order i,X holds
r (#) f is_partial_differentiable_up_to_order i,X
let Z be Subset of (REAL m); :: thesis: for f being PartFunc of (REAL m),REAL
for r being Real st Z is open & f is_partial_differentiable_up_to_order i,Z holds
r (#) f is_partial_differentiable_up_to_order i,Z
let f be PartFunc of (REAL m),REAL; :: thesis: for r being Real st Z is open & f is_partial_differentiable_up_to_order i,Z holds
r (#) f is_partial_differentiable_up_to_order i,Z
let r be Real; :: thesis: ( Z is open & f is_partial_differentiable_up_to_order i,Z implies r (#) f is_partial_differentiable_up_to_order i,Z )
assume AS: ( Z is open & f is_partial_differentiable_up_to_order i,Z ) ; :: thesis: r (#) f is_partial_differentiable_up_to_order i,Z
let I be non empty FinSequence of NAT ; :: according to PDIFF_9:def 10 :: thesis: ( len I <= i & rng I c= Seg m implies r (#) f is_partial_differentiable_on Z,I )
assume P1: ( len I <= i & rng I c= Seg m ) ; :: thesis: r (#) f is_partial_differentiable_on Z,I
then f is_partial_differentiable_on Z,I by AS, TDef9;
hence r (#) f is_partial_differentiable_on Z,I by AS, P1, XCW031; :: thesis: verum