let n be Element of NAT ; :: thesis: for X being set
for f1, f2 being PartFunc of REAL,(REAL n) st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds
( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )
let X be set ; :: thesis: for f1, f2 being PartFunc of REAL,(REAL n) st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds
( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )
let f1, f2 be PartFunc of REAL,(REAL n); :: thesis: ( X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous implies ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous ) )
assume AS: ( X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous ) ; :: thesis: ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )
reconsider g1 = f1, g2 = f2 as PartFunc of REAL, the carrier of (REAL-NS n) by REAL_NS1:def 4;
P2: g1 | X is continuous by AS, Def2Th;
g2 | X is continuous by AS, Def2Th;
then P3: ( (g1 + g2) | X is continuous & (g1 - g2) | X is continuous ) by AS, P2, NFCONT_3:19;
P4: g1 + g2 = f1 + f2 by LM003A;
g1 - g2 = f1 - f2 by LM003D;
hence ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous ) by P3, P4, Def2Th; :: thesis: verum