let X be non empty TopSpace; :: thesis: for S being LinearTopSpace
for f, g being Function of X,S
for x being Point of X st f is_continuous_at x & g is_continuous_at x holds
f + g is_continuous_at x
let S be LinearTopSpace; :: thesis: for f, g being Function of X,S
for x being Point of X st f is_continuous_at x & g is_continuous_at x holds
f + g is_continuous_at x
let f, g be Function of X,S; :: thesis: for x being Point of X st f is_continuous_at x & g is_continuous_at x holds
f + g is_continuous_at x
let x be Point of X; :: thesis: ( f is_continuous_at x & g is_continuous_at x implies f + g is_continuous_at x )
assume A1: ( f is_continuous_at x & g is_continuous_at x ) ; :: thesis: f + g is_continuous_at x
for G being a_neighborhood of (f + g) . x ex H being a_neighborhood of x st (f + g) .: H c= G

proof

let G be a_neighborhood of (f + g) . x; :: thesis: ex H being a_neighborhood of x st (f + g) .: H c= G
A2: dom f = the carrier of X by FUNCT_2:def 1;
A3: dom g = the carrier of X by FUNCT_2:def 1;
A4: dom (f + g) = (dom f) /\ (dom g) by VFUNCT_1:def 1
.= the carrier of X by A2, A3 ;
A5: (f + g) . x = (f + g) /. x
.= (f /. x) + (g /. x) by VFUNCT_1:def 1, A4
.= (f . x) + (g . x) ;
consider W being Subset of S such that
A6: ( W is open & W c= G & (f + g) . x in W ) by CONNSP_2:6;
consider W1, W2 being Subset of S such that
A7: ( W1 is open & W2 is open & f . x in W1 & g . x in W2 & W1 + W2 c= W ) by A5, A6, RLTOPSP1:def 8;
reconsider W1 = W1 as a_neighborhood of f . x by A7, CONNSP_2:3;
reconsider W2 = W2 as a_neighborhood of g . x by A7, CONNSP_2:3;
consider H1 being a_neighborhood of x such that
A8: f .: H1 c= W1 by TMAP_1:def 2, A1;
consider H2 being a_neighborhood of x such that
A9: g .: H2 c= W2 by TMAP_1:def 2, A1;
reconsider H = H1 /\ H2 as a_neighborhood of x by CONNSP_2:2;
take H ; :: thesis: (f + g) .: H c= G
thus (f + g) .: H c= G :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (f + g) .: H or y in G )
assume y in (f + g) .: H ; :: thesis: y in G
then consider z being object such that
A10: ( z in the carrier of X & z in H & y = (f + g) . z ) by FUNCT_2:64;
reconsider z = z as Point of X by A10;
A11: (f + g) . z = (f + g) /. z
.= (f /. z) + (g /. z) by VFUNCT_1:def 1, A4
.= (f . z) + (g . z) ;
z in H1 by XBOOLE_0:def 4, A10;
then A12: f . z in f .: H1 by FUNCT_2:35;
z in H2 by XBOOLE_0:def 4, A10;
then g . z in g .: H2 by FUNCT_2:35;
then (f . z) + (g . z) in W1 + W2 by A12, A8, A9;
hence y in G by A6, A7, A10, A11; :: thesis: verum

end;

end;

hence f + g is_continuous_at x by TMAP_1:def 2; :: thesis: verum