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 that
A1: g1 is continuous and
A2: 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;
A3: 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(A3);
then consider f being Function of the carrier of X,the carrier of (TOP-REAL n) such that
A4: 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) ;
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 (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 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 A6, A7, TOPS_1:55;
reconsider r = g0 . p as Point of (Euclid n) by TOPREAL3:13;
consider r0 being real number such that
A9: r0 > 0 and
A10: Ball r,r0 c= V by A8, 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;
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;
A11: g1 . p in G1 by A9, GOBOARD6:4, XREAL_1:217;
A12: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider GG1 = G1, GG2 = G2 as Subset of (TopSpaceMetr (Euclid n)) ;
GG1 is open by TOPMETR:21;
then G1 is open by A12, PRE_TOPC:60;
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 A1, A11, JGRAPH_2:20;
A16: g2 . p in G2 by A9, GOBOARD6:4, XREAL_1:217;
GG2 is open by TOPMETR:21;
then G2 is open by A12, PRE_TOPC:60;
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 A2, A16, JGRAPH_2:20;
set W = W1 /\ W2;
A20: p in W1 /\ W2 by A13, A17, 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
A21: z in dom g0 and
A22: z in W1 /\ W2 and
A23: g0 . z = x by FUNCT_1:def 12;
A24: z in W1 by A22, XBOOLE_0:def 4;
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 A24, 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 A15, A25, METRIC_1:12;
then A26: |.((g1 . p) - (g1 . pz)).| < r0 / 2 by JGRAPH_1:45;
A27: z in W2 by A22, XBOOLE_0:def 4;
dom g2 = the carrier of X by FUNCT_2:def 1;
then A28: g2 . pz in g2 .: W2 by A27, 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 A19, A28, METRIC_1:12;
then A29: |.((g2 . p) - (g2 . pz)).| < r0 / 2 by JGRAPH_1:45;
A30: aa1 + aa2 = x by A4, A23;
reconsider bb0 = aa1 + aa2 as Point of (Euclid n) by TOPREAL3:13;
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 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 A32: |.(((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 A26, A29, XREAL_1:10;
then |.(((g1 . p) + (g2 . p)) - ((g1 . pz) + (g2 . pz))).| < r0 by A32, XXREAL_0:2;
then |.((g0 . p) - (g0 . pz)).| < r0 by A4, A31;
then dist r,bb0 < r0 by A23, A30, JGRAPH_1:45;
hence x in Ball r,r0 by A30, 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 A10, A14, A18, A20, 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 A5; :: thesis: verum