let X be non empty TopSpace; :: thesis:
let S be LinearTopSpace; :: thesis:
let f, g be Function of X,S; :: thesis:
let x be Point of X; :: thesis:
assume A1: ( f is_continuous_at x & g is_continuous_at x ) ; :: thesis:
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:
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:
thus (f + g) .: H c= G :: thesis:

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in (f + g) .: H ; :: thesis:
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:

end;

end;

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