let X be non empty TopSpace; :: thesis: for n being 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 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_{1}[ 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_{1}[x,y]

for x being Element of X holds S_{1}[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 )

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

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 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

$2 = r1 + r2;

A3: for x being Element of X ex y being Element of (TOP-REAL n) st S

proof

ex f being Function of the carrier of X, the carrier of (TOP-REAL n) st
let x be Element of X; :: thesis: ex y being Element of (TOP-REAL n) st S_{1}[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_{1}[x,y]
; :: thesis: verum

end;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

for x being Element of X holds S

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

then
g0 is continuous
by JGRAPH_2:10;
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:23;

reconsider r = g0 . p as Point of (Euclid n) by TOPREAL3:8;

consider r0 being Real such that

A9: r0 > 0 and

A10: Ball (r,r0) c= V by A8, GOBOARD6:5;

reconsider r01 = g1 . p as Point of (Euclid n) by TOPREAL3:8;

reconsider G1 = Ball (r01,(r0 / 2)) as Subset of (TOP-REAL n) by TOPREAL3:8;

reconsider r02 = g2 . p as Point of (Euclid n) by TOPREAL3:8;

reconsider G2 = Ball (r02,(r0 / 2)) as Subset of (TOP-REAL n) by TOPREAL3:8;

A11: g1 . p in G1 by A9, GOBOARD6:1, XREAL_1:215;

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:14;

then G1 is open by A12, PRE_TOPC:30;

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:10;

A16: g2 . p in G2 by A9, GOBOARD6:1, XREAL_1:215;

GG2 is open by TOPMETR:14;

then G2 is open by A12, PRE_TOPC:30;

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:10;

set W = W1 /\ W2;

A20: p in W1 /\ W2 by A13, A17, XBOOLE_0:def 4;

g0 .: (W1 /\ W2) c= Ball (r,r0)

( p in W & W is open & g0 .: W c= V ) by A10, A14, A18, A20, XBOOLE_1:1; :: thesis: verum

end;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:23;

reconsider r = g0 . p as Point of (Euclid n) by TOPREAL3:8;

consider r0 being Real such that

A9: r0 > 0 and

A10: Ball (r,r0) c= V by A8, GOBOARD6:5;

reconsider r01 = g1 . p as Point of (Euclid n) by TOPREAL3:8;

reconsider G1 = Ball (r01,(r0 / 2)) as Subset of (TOP-REAL n) by TOPREAL3:8;

reconsider r02 = g2 . p as Point of (Euclid n) by TOPREAL3:8;

reconsider G2 = Ball (r02,(r0 / 2)) as Subset of (TOP-REAL n) by TOPREAL3:8;

A11: g1 . p in G1 by A9, GOBOARD6:1, XREAL_1:215;

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:14;

then G1 is open by A12, PRE_TOPC:30;

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:10;

A16: g2 . p in G2 by A9, GOBOARD6:1, XREAL_1:215;

GG2 is open by TOPMETR:14;

then G2 is open by A12, PRE_TOPC:30;

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:10;

set W = W1 /\ W2;

A20: p in W1 /\ W2 by A13, A17, XBOOLE_0:def 4;

g0 .: (W1 /\ W2) c= Ball (r,r0)

proof

hence
ex W being Subset of X st
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 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 6;

reconsider aa1 = g1 . pz as Point of (TOP-REAL n) ;

reconsider bb1 = aa1 as Point of (Euclid n) by TOPREAL3:8;

dist (r01,bb1) < r0 / 2 by A15, A25, METRIC_1:11;

then A26: |.((g1 . p) - (g1 . pz)).| < r0 / 2 by JGRAPH_1:28;

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 6;

reconsider aa2 = g2 . pz as Point of (TOP-REAL n) ;

reconsider bb2 = aa2 as Point of (Euclid n) by TOPREAL3:8;

dist (r02,bb2) < r0 / 2 by A19, A28, METRIC_1:11;

then A29: |.((g2 . p) - (g2 . pz)).| < r0 / 2 by JGRAPH_1:28;

A30: aa1 + aa2 = x by A4, A23;

reconsider bb0 = aa1 + aa2 as Point of (Euclid n) 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 A26, A29, XREAL_1:8;

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:28;

hence x in Ball (r,r0) by A30, METRIC_1:11; :: thesis: verum

end;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 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 6;

reconsider aa1 = g1 . pz as Point of (TOP-REAL n) ;

reconsider bb1 = aa1 as Point of (Euclid n) by TOPREAL3:8;

dist (r01,bb1) < r0 / 2 by A15, A25, METRIC_1:11;

then A26: |.((g1 . p) - (g1 . pz)).| < r0 / 2 by JGRAPH_1:28;

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 6;

reconsider aa2 = g2 . pz as Point of (TOP-REAL n) ;

reconsider bb2 = aa2 as Point of (Euclid n) by TOPREAL3:8;

dist (r02,bb2) < r0 / 2 by A19, A28, METRIC_1:11;

then A29: |.((g2 . p) - (g2 . pz)).| < r0 / 2 by JGRAPH_1:28;

A30: aa1 + aa2 = x by A4, A23;

reconsider bb0 = aa1 + aa2 as Point of (Euclid n) 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 A26, A29, XREAL_1:8;

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:28;

hence x in Ball (r,r0) by A30, METRIC_1:11; :: thesis: verum

( p in W & W is open & g0 .: W c= V ) by A10, A14, A18, A20, XBOOLE_1:1; :: thesis: verum

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