let X be non empty TopSpace; :: thesis: for n being Element of NAT
for g1, g2 being Function of X,(TOP-REAL n) st g1 is continuous & g2 is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous )
let n be Element of NAT ; :: thesis: for g1, g2 being Function of X,(TOP-REAL n) st g1 is continuous & g2 is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous )
let g1, g2 be Function of X,(TOP-REAL n); :: thesis: ( g1 is continuous & g2 is continuous implies ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous ) )
assume A1: ( g1 is continuous & g2 is continuous ) ; :: thesis: ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous )
defpred S₁[ set , set ] means for r1, r2 being Element of (TOP-REAL n) st g1 . $1 = r1 & g2 . $1 = r2 holds
$2 = r1 + r2;
A2: for x being Element of X ex y being Element of (TOP-REAL n) st S₁[x,y]

proof

let x be Element of X; :: thesis: ex y being Element of (TOP-REAL n) st S₁[x,y]
set rr1 = g1 . x;
set rr2 = g2 . x;
set r3 = (g1 . x) + (g2 . x);
for s1, s2 being Point of (TOP-REAL n) st g1 . x = s1 & g2 . x = s2 holds
(g1 . x) + (g2 . x) = s1 + s2 ;
hence ex y being Element of (TOP-REAL n) st S₁[x,y] ; :: thesis: verum

end;

ex f being Function of the carrier of X,the carrier of (TOP-REAL n) st
for x being Element of X holds S₁[x,f . x] from FUNCT_2:sch 3(A2);
then consider f being Function of the carrier of X,the carrier of (TOP-REAL n) such that
A3: for x being Element of X
for r1, r2 being Element of (TOP-REAL n) st g1 . x = r1 & g2 . x = r2 holds
f . x = r1 + r2 ;
reconsider g0 = f as Function of X,(TOP-REAL n) ;
A4: for r being Point of X holds g0 . r = (g1 . r) + (g2 . r) by A3;
for p being Point of X
for V being Subset of (TOP-REAL n) 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 (TOP-REAL n) 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 (TOP-REAL n); :: 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 ( g0 . p in V & V is open ) ; :: thesis: ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
then A5: g0 . p in Int V by TOPS_1:55;
reconsider r = g0 . p as Point of (Euclid n) by TOPREAL3:13;
consider r0 being real number such that
A6: ( r0 > 0 & Ball r,r0 c= V ) by A5, GOBOARD6:8;
reconsider r01 = g1 . p as Point of (Euclid n) by TOPREAL3:13;
reconsider G1 = Ball r01,(r0 / 2) as Subset of (TOP-REAL n) by TOPREAL3:13;
A7: r0 / 2 > 0 by A6, XREAL_1:217;
then A8: g1 . p in G1 by GOBOARD6:4;
G1 is open by TOPMETR:21;
then consider W1 being Subset of X such that
A9: ( p in W1 & W1 is open & g1 .: W1 c= G1 ) by A1, A8, JGRAPH_2:20;
reconsider r02 = g2 . p as Point of (Euclid n) by TOPREAL3:13;
reconsider G2 = Ball r02,(r0 / 2) as Subset of (TOP-REAL n) by TOPREAL3:13;
A10: g2 . p in G2 by A7, GOBOARD6:4;
G2 is open by TOPMETR:21;
then consider W2 being Subset of X such that
A11: ( p in W2 & W2 is open & g2 .: W2 c= G2 ) by A1, A10, JGRAPH_2:20;
set W = W1 /\ W2;
A12: W1 /\ W2 is open by A9, A11, TOPS_1:38;
A13: p in W1 /\ W2 by A9, A11, XBOOLE_0:def 4;
g0 .: (W1 /\ W2) c= Ball r,r0

proof

let x be set ; :: 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 set such that
A14: ( z in dom g0 & z in W1 /\ W2 & g0 . z = x ) by FUNCT_1:def 12;
A15: z in W1 by A14, XBOOLE_0:def 4;
reconsider pz = z as Point of X by A14;
dom g1 = the carrier of X by FUNCT_2:def 1;
then A16: g1 . pz in g1 .: W1 by A15, FUNCT_1:def 12;
reconsider aa1 = g1 . pz as Point of (TOP-REAL n) ;
reconsider bb1 = aa1 as Point of (Euclid n) by TOPREAL3:13;
dist r01,bb1 < r0 / 2 by A9, A16, METRIC_1:12;
then A17: |.((g1 . p) - (g1 . pz)).| < r0 / 2 by JGRAPH_1:45;
A18: z in W2 by A14, XBOOLE_0:def 4;
dom g2 = the carrier of X by FUNCT_2:def 1;
then A19: g2 . pz in g2 .: W2 by A18, FUNCT_1:def 12;
reconsider aa2 = g2 . pz as Point of (TOP-REAL n) ;
reconsider bb2 = aa2 as Point of (Euclid n) by TOPREAL3:13;
dist r02,bb2 < r0 / 2 by A11, A19, METRIC_1:12;
then A20: |.((g2 . p) - (g2 . pz)).| < r0 / 2 by JGRAPH_1:45;
A21: aa1 + aa2 = x by A3, A14;
reconsider bb0 = aa1 + aa2 as Point of (Euclid n) by TOPREAL3:13;
A22: g0 . pz = (g1 . pz) + (g2 . pz) by A3;
((g1 . p) + (g2 . p)) - ((g1 . pz) + (g2 . pz)) = (((g1 . p) + (g2 . p)) - (g1 . pz)) - (g2 . pz) by EUCLID:50
.= (((g1 . p) + (g2 . p)) + (- (g1 . pz))) - (g2 . pz) by EUCLID:45
.= (((g1 . p) + (g2 . p)) + (- (g1 . pz))) + (- (g2 . pz)) by EUCLID:45
.= (((g1 . p) + (- (g1 . pz))) + (g2 . p)) + (- (g2 . pz)) by EUCLID:30
.= ((g1 . p) + (- (g1 . pz))) + ((g2 . p) + (- (g2 . pz))) by EUCLID:30
.= ((g1 . p) - (g1 . pz)) + ((g2 . p) + (- (g2 . pz))) by EUCLID:45
.= ((g1 . p) - (g1 . pz)) + ((g2 . p) - (g2 . pz)) by EUCLID:45 ;
then A23: |.(((g1 . p) + (g2 . p)) - ((g1 . pz) + (g2 . pz))).| <= |.((g1 . p) - (g1 . pz)).| + |.((g2 . p) - (g2 . pz)).| by TOPRNS_1:30;
|.((g1 . p) - (g1 . pz)).| + |.((g2 . p) - (g2 . pz)).| < (r0 / 2) + (r0 / 2) by A17, A20, XREAL_1:10;
then |.(((g1 . p) + (g2 . p)) - ((g1 . pz) + (g2 . pz))).| < r0 by A23, XXREAL_0:2;
then |.((g0 . p) - (g0 . pz)).| < r0 by A3, A22;
then dist r,bb0 < r0 by A14, A21, JGRAPH_1:45;
hence x in Ball r,r0 by A21, METRIC_1:12; :: thesis: verum

end;

hence ex W being Subset of X st
( p in W & W is open & g0 .: W c= V ) by A6, A12, A13, XBOOLE_1:1; :: thesis: verum

end;

then g0 is continuous by JGRAPH_2:20;
hence ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous ) by A4; :: thesis: verum