theorem :: NFCONT_3:12

for x0 being Real
for S being RealNormSpace
for f1, f2 being PartFunc of REAL, the carrier of S st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 )