theorem :: FCONT_1:27

for f being PartFunc of REAL,REAL st f is total & ( for x1, x2 being Real holds f . (x1 + x2) = (f . x1) + (f . x2) ) & ex x0 being Real st f is_continuous_in x0 holds
f | REAL is continuous