let m be non zero 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 A1: ( 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 11 :: thesis: ( len I <= i & rng I c= Seg m implies r (#) f is_partial_differentiable_on Z,I )
assume A2: ( 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 A1;
hence r (#) f is_partial_differentiable_on Z,I by A1, A2, Th79; :: thesis: verum