let n be Element of NAT ; for X, X1 being set
for f1, f2 being PartFunc of REAL,(REAL n) st X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous holds
( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous )
let X, X1 be set ; for f1, f2 being PartFunc of REAL,(REAL n) st X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous holds
( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous )
let f1, f2 be PartFunc of REAL,(REAL n); ( X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous implies ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) )
assume A1:
( X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous )
; ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous )
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
A2:
g1 | X is continuous
by A1, Th23;
g2 | X1 is continuous
by A1, Th23;
then A3:
( (g1 + g2) | (X /\ X1) is continuous & (g1 - g2) | (X /\ X1) is continuous )
by A1, A2, NFCONT_3:20;
A4:
g1 + g2 = f1 + f2
by Th5;
g1 - g2 = f1 - f2
by Th10;
hence
( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous )
by A3, A4, Th23; verum