theorem :: FUZNUM_1:23

for f, g being PartFunc of REAL,REAL st f is continuous & g is continuous & ex x being object st
( (dom f) /\ (dom g) = {x} & ( for x being object st x in (dom f) /\ (dom g) holds
f . x = g . x ) ) holds
ex h being PartFunc of REAL,REAL st
( h = f +* g & ( for x being Real st x in (dom f) /\ (dom g) holds
h is_continuous_in x ) )