let X be non empty TopSpace; :: thesis: for n being Nat
for g1, g2 being Function of X,() st g1 is continuous & g2 is continuous holds
ex g being Function of X,() st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous )

let n be Nat; :: thesis: for g1, g2 being Function of X,() st g1 is continuous & g2 is continuous holds
ex g being Function of X,() st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous )

let g1, g2 be Function of X,(); :: thesis: ( g1 is continuous & g2 is continuous implies ex g being Function of X,() st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous ) )

assume that
A1: g1 is continuous and
A2: g2 is continuous ; :: thesis: ex g being Function of X,() st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous )

defpred S1[ set , set ] means for r1, r2 being Element of () st g1 . \$1 = r1 & g2 . \$1 = r2 holds
\$2 = r1 + r2;
A3: for x being Element of X ex y being Element of () st S1[x,y]
proof
let x be Element of X; :: thesis: ex y being Element of () st S1[x,y]
set rr1 = g1 . x;
set rr2 = g2 . x;
set r3 = (g1 . x) + (g2 . x);
for s1, s2 being Point of () st g1 . x = s1 & g2 . x = s2 holds
(g1 . x) + (g2 . x) = s1 + s2 ;
hence ex y being Element of () st S1[x,y] ; :: thesis: verum
end;
ex f being Function of the carrier of X, the carrier of () st
for x being Element of X holds S1[x,f . x] from then consider f being Function of the carrier of X, the carrier of () such that
A4: for x being Element of X
for r1, r2 being Element of () st g1 . x = r1 & g2 . x = r2 holds
f . x = r1 + r2 ;
reconsider g0 = f as Function of X,() ;
A5: for r being Point of X holds g0 . r = (g1 . r) + (g2 . r) by A4;
for p being Point of X
for V being Subset of () st g0 . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
proof
let p be Point of X; :: thesis: for V being Subset of () st g0 . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )

let V be Subset of (); :: thesis: ( g0 . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) )

assume that
A6: g0 . p in V and
A7: V is open ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )

A8: g0 . p in Int V by ;
reconsider r = g0 . p as Point of () by TOPREAL3:8;
consider r0 being Real such that
A9: r0 > 0 and
A10: Ball (r,r0) c= V by ;
reconsider r01 = g1 . p as Point of () by TOPREAL3:8;
reconsider G1 = Ball (r01,(r0 / 2)) as Subset of () by TOPREAL3:8;
reconsider r02 = g2 . p as Point of () by TOPREAL3:8;
reconsider G2 = Ball (r02,(r0 / 2)) as Subset of () by TOPREAL3:8;
A11: g1 . p in G1 by ;
A12: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
then reconsider GG1 = G1, GG2 = G2 as Subset of () ;
GG1 is open by TOPMETR:14;
then G1 is open by ;
then consider W1 being Subset of X such that
A13: p in W1 and
A14: W1 is open and
A15: g1 .: W1 c= G1 by ;
A16: g2 . p in G2 by ;
GG2 is open by TOPMETR:14;
then G2 is open by ;
then consider W2 being Subset of X such that
A17: p in W2 and
A18: W2 is open and
A19: g2 .: W2 c= G2 by ;
set W = W1 /\ W2;
A20: p in W1 /\ W2 by ;
g0 .: (W1 /\ W2) c= Ball (r,r0)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g0 .: (W1 /\ W2) or x in Ball (r,r0) )
assume x in g0 .: (W1 /\ W2) ; :: thesis: x in Ball (r,r0)
then consider z being object such that
A21: z in dom g0 and
A22: z in W1 /\ W2 and
A23: g0 . z = x by FUNCT_1:def 6;
A24: z in W1 by ;
reconsider pz = z as Point of X by A21;
dom g1 = the carrier of X by FUNCT_2:def 1;
then A25: g1 . pz in g1 .: W1 by ;
reconsider aa1 = g1 . pz as Point of () ;
reconsider bb1 = aa1 as Point of () by TOPREAL3:8;
dist (r01,bb1) < r0 / 2 by ;
then A26: |.((g1 . p) - (g1 . pz)).| < r0 / 2 by JGRAPH_1:28;
A27: z in W2 by ;
dom g2 = the carrier of X by FUNCT_2:def 1;
then A28: g2 . pz in g2 .: W2 by ;
reconsider aa2 = g2 . pz as Point of () ;
reconsider bb2 = aa2 as Point of () by TOPREAL3:8;
dist (r02,bb2) < r0 / 2 by ;
then A29: |.((g2 . p) - (g2 . pz)).| < r0 / 2 by JGRAPH_1:28;
A30: aa1 + aa2 = x by ;
reconsider bb0 = aa1 + aa2 as Point of () by TOPREAL3:8;
A31: g0 . pz = (g1 . pz) + (g2 . pz) by A4;
((g1 . p) + (g2 . p)) - ((g1 . pz) + (g2 . pz)) = (((g1 . p) + (g2 . p)) - (g1 . pz)) - (g2 . pz) by RLVECT_1:27
.= (((g1 . p) + (g2 . p)) + (- (g1 . pz))) - (g2 . pz)
.= (((g1 . p) + (g2 . p)) + (- (g1 . pz))) + (- (g2 . pz))
.= (((g1 . p) + (- (g1 . pz))) + (g2 . p)) + (- (g2 . pz)) by RLVECT_1:def 3
.= ((g1 . p) + (- (g1 . pz))) + ((g2 . p) + (- (g2 . pz))) by RLVECT_1:def 3
.= ((g1 . p) - (g1 . pz)) + ((g2 . p) + (- (g2 . pz)))
.= ((g1 . p) - (g1 . pz)) + ((g2 . p) - (g2 . pz)) ;
then A32: |.(((g1 . p) + (g2 . p)) - ((g1 . pz) + (g2 . pz))).| <= |.((g1 . p) - (g1 . pz)).| + |.((g2 . p) - (g2 . pz)).| by TOPRNS_1:29;
|.((g1 . p) - (g1 . pz)).| + |.((g2 . p) - (g2 . pz)).| < (r0 / 2) + (r0 / 2) by ;
then |.(((g1 . p) + (g2 . p)) - ((g1 . pz) + (g2 . pz))).| < r0 by ;
then |.((g0 . p) - (g0 . pz)).| < r0 by ;
then dist (r,bb0) < r0 by ;
hence x in Ball (r,r0) by ; :: thesis: verum
end;
hence ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) by ; :: thesis: verum
end;
then g0 is continuous by JGRAPH_2:10;
hence ex g being Function of X,() st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous ) by A5; :: thesis: verum