theorem Th5: :: CKSPACE1:5

for m being non zero Element of NAT
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