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

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