let m be non zero Element of NAT ; for k being Element of NAT
for X being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for d being Real st X is open & f = X --> d holds
f is_continuously_differentiable_up_to_order k,X
let k be Element of NAT ; for X being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for d being Real st X is open & f = X --> d holds
f is_continuously_differentiable_up_to_order k,X
let X be non empty Subset of (REAL m); for f being PartFunc of (REAL m),REAL
for d being Real st X is open & f = X --> d holds
f is_continuously_differentiable_up_to_order k,X
let f be PartFunc of (REAL m),REAL; for d being Real st X is open & f = X --> d holds
f is_continuously_differentiable_up_to_order k,X
let d be Real; ( X is open & f = X --> d implies f is_continuously_differentiable_up_to_order k,X )
assume A1:
( X is open & f = X --> d )
; f is_continuously_differentiable_up_to_order k,X
then
f is_partial_differentiable_up_to_order k,X
by Th18;
hence
f is_continuously_differentiable_up_to_order k,X
by A1, Th18, FUNCT_2:def 1; verum