theorem Th13: :: NFCONT_3:13

for r, x0 being Real
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st f is_continuous_in x0 holds
r (#) f is_continuous_in x0