let m be non empty Element of NAT ; :: thesis: for f, g being PartFunc of (REAL m),REAL
for x0 being Element of REAL m st f is_continuous_in x0 & g is_continuous_in x0 holds
( f + g is_continuous_in x0 & f - g is_continuous_in x0 )
let f, g be PartFunc of (REAL m),REAL; :: thesis: for x0 being Element of REAL m st f is_continuous_in x0 & g is_continuous_in x0 holds
( f + g is_continuous_in x0 & f - g is_continuous_in x0 )
let x0 be Element of REAL m; :: thesis: ( f is_continuous_in x0 & g is_continuous_in x0 implies ( f + g is_continuous_in x0 & f - g is_continuous_in x0 ) )
assume ( f is_continuous_in x0 & g is_continuous_in x0 ) ; :: thesis: ( f + g is_continuous_in x0 & f - g is_continuous_in x0 )
then ( <>* f is_continuous_in x0 & <>* g is_continuous_in x0 ) by XTh35;
then A2: ( (<>* f) + (<>* g) is_continuous_in x0 & (<>* f) - (<>* g) is_continuous_in x0 ) by XTh350;
( (<>* f) + (<>* g) = <>* (f + g) & (<>* f) - (<>* g) = <>* (f - g) ) by LMXTh10;
hence ( f + g is_continuous_in x0 & f - g is_continuous_in x0 ) by A2, XTh35; :: thesis: verum