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 r being Real
for f being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & X is open holds
r (#) 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 r being Real
for f being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & X is open holds
r (#) f is_continuously_differentiable_up_to_order k,X

let X be non empty Subset of (REAL m); :: thesis: for r being Real
for f being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & X is open holds
r (#) f is_continuously_differentiable_up_to_order k,X

let r be Real; :: thesis: for f being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & X is open holds
r (#) f is_continuously_differentiable_up_to_order k,X

let f be PartFunc of (REAL m),REAL; :: thesis:
assume A1: ( f is_continuously_differentiable_up_to_order k,X & X is open ) ; :: thesis:
for I being non empty FinSequence of NAT st len I <= k & rng I c= Seg m holds
(r (#) f) `partial| (X,I) is_continuous_on X
proof
let I be non empty FinSequence of NAT ; :: thesis: ( len I <= k & rng I c= Seg m implies (r (#) f) `partial| (X,I) is_continuous_on X )
assume A2: ( len I <= k & rng I c= Seg m ) ; :: thesis: (r (#) f) `partial| (X,I) is_continuous_on X
A3: f is_partial_differentiable_on X,I by ;
reconsider f0 = f `partial| (X,I) as PartFunc of (REAL m),REAL ;
X = dom f0 by ;
then r (#) f0 is_continuous_on X by ;
hence (r (#) f) `partial| (X,I) is_continuous_on X by ; :: thesis: verum
end;
hence r (#) f is_continuously_differentiable_up_to_order k,X by ; :: thesis: verum