theorem Th8: :: FCONT_1:8

for r, x0 being Real
for f being PartFunc of REAL,REAL st x0 in dom f & f is_continuous_in x0 holds
r (#) f is_continuous_in x0