let m, n be non zero Element of NAT ; for f, g being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_continuous_in x & g is_continuous_in x holds
( f + g is_continuous_in x & f - g is_continuous_in x )
let f, g be PartFunc of (REAL m),(REAL n); for x being Element of REAL m st f is_continuous_in x & g is_continuous_in x holds
( f + g is_continuous_in x & f - g is_continuous_in x )
let x be Element of REAL m; ( f is_continuous_in x & g is_continuous_in x implies ( f + g is_continuous_in x & f - g is_continuous_in x ) )
assume A1:
( f is_continuous_in x & g is_continuous_in x )
; ( f + g is_continuous_in x & f - g is_continuous_in x )
reconsider y = x as Point of (REAL-NS m) by REAL_NS1:def 4;
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) ;
A3:
( f1 + g1 is_continuous_in y & f1 - g1 is_continuous_in y )
by NFCONT_1:15, A1;
( f + g = f1 + g1 & f - g = f1 - g1 )
by A2, NFCONT_4:5, NFCONT_4:10;
hence
( f + g is_continuous_in x & f - g is_continuous_in x )
by A3; verum