let m be non zero Element of NAT ; :: thesis: 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 ; :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: ( X is open & f = X --> d implies f is_continuously_differentiable_up_to_order k,X )
assume A1: ( X is open & f = X --> d ) ; :: thesis: 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; :: thesis: verum