let m be non zero Element of NAT ; 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 ; 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); 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; 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; ( 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 )
; r (#) f is_partial_differentiable_up_to_order i,Z
let I be non empty FinSequence of NAT ; PDIFF_9:def 11 ( 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 )
; 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; verum