let x0 be real number ; :: thesis: for S being RealNormSpace
for f1, f2 being PartFunc of REAL, the carrier of S st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 )
let S be RealNormSpace; :: thesis: for f1, f2 being PartFunc of REAL, the carrier of S st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 )
let f1, f2 be PartFunc of REAL, the carrier of S; :: thesis: ( x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 implies ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 ) )
assume A1: x0 in (dom f1) /\ (dom f2) ; :: thesis: ( not f1 is_continuous_in x0 or not f2 is_continuous_in x0 or ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 ) )
assume A2: ( f1 is_continuous_in x0 & f2 is_continuous_in x0 ) ; :: thesis: ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 )
Y1: dom (f1 + f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def 1;
Y0: x0 in dom (f1 + f2) by A1, VFUNCT_1:def 1;

now

let s1 be Real_Sequence; :: thesis: ( rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 = x0 implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) ) )
assume that
A4: rng s1 c= dom (f1 + f2) and
A5: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) )
A6: rng s1 c= (dom f1) /\ (dom f2) by A4, VFUNCT_1:def 1;
( dom (f1 + f2) c= dom f1 & dom (f1 + f2) c= dom f2 ) by Y1, XBOOLE_1:17;
then A7: ( rng s1 c= dom f1 & rng s1 c= dom f2 ) by A4, XBOOLE_1:1;
then A8: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A2, A5, Def1;
then (f1 /* s1) + (f2 /* s1) is convergent by NORMSP_1:34;
hence (f1 + f2) /* s1 is convergent by A6, XTh19; :: thesis: (f1 + f2) /. x0 = lim ((f1 + f2) /* s1)
A9: ( f1 /. x0 = lim (f1 /* s1) & f2 /. x0 = lim (f2 /* s1) ) by A2, A5, A7, Def1;
thus (f1 + f2) /. x0 = (f1 /. x0) + (f2 /. x0) by Y0, VFUNCT_1:def 1
.= lim ((f1 /* s1) + (f2 /* s1)) by A8, A9, NORMSP_1:42
.= lim ((f1 + f2) /* s1) by A6, XTh19 ; :: thesis: verum

end;

hence f1 + f2 is_continuous_in x0 by Y0, Def1; :: thesis: f1 - f2 is_continuous_in x0
Y1: dom (f1 - f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def 2;
Y0: x0 in dom (f1 - f2) by A1, VFUNCT_1:def 2;

now

let s1 be Real_Sequence; :: thesis: ( rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 = x0 implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) ) )
assume that
A13: rng s1 c= dom (f1 - f2) and
A14: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) )
A15: rng s1 c= (dom f1) /\ (dom f2) by A13, VFUNCT_1:def 2;
( dom (f1 - f2) c= dom f1 & dom (f1 - f2) c= dom f2 ) by Y1, XBOOLE_1:17;
then A16: ( rng s1 c= dom f1 & rng s1 c= dom f2 ) by A13, XBOOLE_1:1;
then A17: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A2, A14, Def1;
then (f1 /* s1) - (f2 /* s1) is convergent by NORMSP_1:35;
hence (f1 - f2) /* s1 is convergent by A15, XTh19; :: thesis: (f1 - f2) /. x0 = lim ((f1 - f2) /* s1)
A20: ( f1 /. x0 = lim (f1 /* s1) & f2 /. x0 = lim (f2 /* s1) ) by A2, A14, A16, Def1;
thus (f1 - f2) /. x0 = (f1 /. x0) - (f2 /. x0) by Y0, VFUNCT_1:def 2
.= lim ((f1 /* s1) - (f2 /* s1)) by A20, A17, NORMSP_1:43
.= lim ((f1 - f2) /* s1) by A15, XTh19 ; :: thesis: verum

end;

hence f1 - f2 is_continuous_in x0 by Y0, Def1; :: thesis: verum