let m, n be non zero Element of NAT ; :: thesis: for Z being set
for f, g being PartFunc of (REAL m),(REAL n) st f is_continuous_on Z & g is_continuous_on Z 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 n) st f is_continuous_on Z & g is_continuous_on Z holds
( f + g is_continuous_on Z & f - g is_continuous_on Z )
let f, g be PartFunc of (REAL m),(REAL n); :: thesis: ( f is_continuous_on Z & g is_continuous_on Z implies ( f + g is_continuous_on Z & f - g is_continuous_on Z ) )
assume A1: ( f is_continuous_on Z & g is_continuous_on Z ) ; :: thesis: ( f + g is_continuous_on Z & f - g is_continuous_on Z )
A2: ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then reconsider f1 = f, g1 = g as PartFunc of (REAL-NS m),(REAL-NS n) ;
( f1 is_continuous_on Z & g1 is_continuous_on Z ) by A1, PDIFF_7:37;
then A3: ( f1 + g1 is_continuous_on Z & f1 - g1 is_continuous_on Z ) by NFCONT_1:25;
( f + g = f1 + g1 & f - g = f1 - g1 ) by A2, NFCONT_4:5, NFCONT_4:10;
hence ( f + g is_continuous_on Z & f - g is_continuous_on Z ) by A3, PDIFF_7:37; :: thesis: verum