let m be non zero Element of NAT ; :: thesis: for Z being set
for f, g being PartFunc of (REAL m),REAL st f is_continuous_on Z & g is_continuous_on Z & Z c= dom f & Z c= dom g holds
( f + g is_continuous_on Z & f - g is_continuous_on Z )
let Z be set ; :: thesis: for f, g being PartFunc of (REAL m),REAL st f is_continuous_on Z & g is_continuous_on Z & Z c= dom f & Z c= dom g holds
( f + g is_continuous_on Z & f - g is_continuous_on Z )
let f, g be PartFunc of (REAL m),REAL; :: thesis: ( f is_continuous_on Z & g is_continuous_on Z & Z c= dom f & Z c= dom g implies ( f + g is_continuous_on Z & f - g is_continuous_on Z ) )
assume ( f is_continuous_on Z & g is_continuous_on Z & Z c= dom f & Z c= dom g ) ; :: thesis: ( f + g is_continuous_on Z & f - g is_continuous_on Z )
then ( <>* f is_continuous_on Z & <>* g is_continuous_on Z ) by Th44;
then A1: ( (<>* f) + (<>* g) is_continuous_on Z & (<>* f) - (<>* g) is_continuous_on Z ) by Th33;
( (<>* f) + (<>* g) = <>* (f + g) & (<>* f) - (<>* g) = <>* (f - g) ) by Th7;
hence ( f + g is_continuous_on Z & f - g is_continuous_on Z ) by A1, Th44; :: thesis: verum