for m being non zero Element of NAT
for Z being non empty Subset of (REAL m) st Z is open holds
for k being Element of NAT
for f, g being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,Z & g is_continuously_differentiable_up_to_order k,Z holds
f (#) g is_continuously_differentiable_up_to_order k,Z