let S be RealNormSpace; :: thesis: for X being set
for f1, f2 being PartFunc of REAL, the carrier of S 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, the carrier of S 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, the carrier of S; :: 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 that
A1: X c= (dom f1) /\ (dom f2) and
A2: ( f1 | X is continuous & f2 | X is continuous ) ; :: thesis: ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )
A3: ( X c= dom f1 & X c= dom f2 ) by A1, XBOOLE_1:18;
A4: ( X c= dom (f1 + f2) & X c= dom (f1 - f2) ) by A1, VFUNCT_1:def 1, VFUNCT_1:def 2;

now :: thesis: for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) )

let s1 be Real_Sequence; :: thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) )
assume that
A5: ( rng s1 c= X & s1 is convergent ) and
A6: lim s1 in X ; :: thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) )
A7: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A3, A2, A5, A6, Th16;
then A8: (f1 /* s1) + (f2 /* s1) is convergent by NORMSP_1:19;
A9: rng s1 c= (dom f1) /\ (dom f2) by A1, A5, XBOOLE_1:1;
A10: lim s1 in REAL by XREAL_0:def 1;
( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A3, A2, A5, A6, Th16;
then (f1 + f2) /. (lim s1) = (lim (f1 /* s1)) + (lim (f2 /* s1)) by A4, A6, VFUNCT_1:def 1, A10
.= lim ((f1 /* s1) + (f2 /* s1)) by A7, NORMSP_1:25
.= lim ((f1 + f2) /* s1) by A9, Th2 ;
hence ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) by A9, A8, Th2; :: thesis: verum

end;

hence (f1 + f2) | X is continuous by A4, Th16; :: thesis: (f1 - f2) | X is continuous

now :: thesis: for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) )

let s1 be Real_Sequence; :: thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) )
assume that
A11: ( rng s1 c= X & s1 is convergent ) and
A12: lim s1 in X ; :: thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) )
A13: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A3, A2, A11, A12, Th16;
then A14: (f1 /* s1) - (f2 /* s1) is convergent by NORMSP_1:20;
A15: rng s1 c= (dom f1) /\ (dom f2) by A1, A11, XBOOLE_1:1;
A16: lim s1 in REAL by XREAL_0:def 1;
( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A3, A2, A11, A12, Th16;
then (f1 - f2) /. (lim s1) = (lim (f1 /* s1)) - (lim (f2 /* s1)) by A4, A12, VFUNCT_1:def 2, A16
.= lim ((f1 /* s1) - (f2 /* s1)) by A13, NORMSP_1:26
.= lim ((f1 - f2) /* s1) by A15, Th2 ;
hence ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) by A15, A14, Th2; :: thesis: verum

end;

hence (f1 - f2) | X is continuous by A4, Th16; :: thesis: verum