let S be RealNormSpace; :: thesis: for X, X1 being set
for f1, f2 being PartFunc of REAL, the carrier of S 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 ; :: thesis: for f1, f2 being PartFunc of REAL, the carrier of S 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, the carrier of S; :: thesis: ( 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 ( X c= dom f1 & X1 c= dom f2 ) ; :: thesis: ( not f1 | X is continuous or not f2 | X1 is continuous or ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) )
then A1: X /\ X1 c= (dom f1) /\ (dom f2) by XBOOLE_1:27;
assume ( f1 | X is continuous & f2 | X1 is continuous ) ; :: thesis: ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous )
then ( f1 | (X /\ X1) is continuous & f2 | (X /\ X1) is continuous ) by Th18, XBOOLE_1:17;
hence ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) by A1, Th19; :: thesis: verum