theorem :: NFCONT_4:16
for n being Element of NAT
for r, x0 being Real
for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds
r (#) f is_continuous_in x0