let X be non empty TopSpace; for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 + r2 ) & g is continuous )
let f1, f2 be Function of X,R^1; ( f1 is continuous & f2 is continuous implies ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 + r2 ) & g is continuous ) )
assume that
A1:
f1 is continuous
and
A2:
f2 is continuous
; ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 + r2 ) & g is continuous )
defpred S1[ set , set ] means for r1, r2 being Real st f1 . $1 = r1 & f2 . $1 = r2 holds
$2 = r1 + r2;
A3:
for x being Element of X ex y being Element of REAL st S1[x,y]
ex f being Function of the carrier of X,REAL st
for x being Element of X holds S1[x,f . x]
from FUNCT_2:sch 3(A3);
then consider f being Function of the carrier of X,REAL such that
A4:
for x being Element of X
for r1, r2 being Real st f1 . x = r1 & f2 . x = r2 holds
f . x = r1 + r2
;
reconsider g0 = f as Function of X,R^1 by TOPMETR:17;
for p being Point of X
for V being Subset of R^1 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;
for V being Subset of R^1 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
R^1;
( 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 ) )
reconsider r =
g0 . p as
Real ;
reconsider r1 =
f1 . p as
Real ;
reconsider r2 =
f2 . p as
Real ;
assume
(
g0 . p in V &
V is
open )
;
ex W being Subset of X st
( p in W & W is open & g0 .: W c= V )
then consider r0 being
Real such that A5:
r0 > 0
and A6:
].(r - r0),(r + r0).[ c= V
by FRECHET:8;
reconsider G1 =
].(r1 - (r0 / 2)),(r1 + (r0 / 2)).[ as
Subset of
R^1 by TOPMETR:17;
A7:
r1 < r1 + (r0 / 2)
by A5, XREAL_1:29, XREAL_1:215;
then
r1 - (r0 / 2) < r1
by XREAL_1:19;
then A8:
f1 . p in G1
by A7, XXREAL_1:4;
reconsider G2 =
].(r2 - (r0 / 2)),(r2 + (r0 / 2)).[ as
Subset of
R^1 by TOPMETR:17;
A9:
r2 < r2 + (r0 / 2)
by A5, XREAL_1:29, XREAL_1:215;
then
r2 - (r0 / 2) < r2
by XREAL_1:19;
then A10:
f2 . p in G2
by A9, XXREAL_1:4;
G2 is
open
by JORDAN6:35;
then consider W2 being
Subset of
X such that A11:
(
p in W2 &
W2 is
open )
and A12:
f2 .: W2 c= G2
by A2, A10, Th10;
G1 is
open
by JORDAN6:35;
then consider W1 being
Subset of
X such that A13:
(
p in W1 &
W1 is
open )
and A14:
f1 .: W1 c= G1
by A1, A8, Th10;
set W =
W1 /\ W2;
A15:
g0 .: (W1 /\ W2) c= ].(r - r0),(r + r0).[
proof
let x be
object ;
TARSKI:def 3 ( not x in g0 .: (W1 /\ W2) or x in ].(r - r0),(r + r0).[ )
assume
x in g0 .: (W1 /\ W2)
;
x in ].(r - r0),(r + r0).[
then consider z being
object such that A16:
z in dom g0
and A17:
z in W1 /\ W2
and A18:
g0 . z = x
by FUNCT_1:def 6;
reconsider pz =
z as
Point of
X by A16;
reconsider aa2 =
f2 . pz as
Real ;
reconsider aa1 =
f1 . pz as
Real ;
A19:
pz in the
carrier of
X
;
then A20:
pz in dom f2
by FUNCT_2:def 1;
z in W2
by A17, XBOOLE_0:def 4;
then A21:
f2 . pz in f2 .: W2
by A20, FUNCT_1:def 6;
then A22:
r2 - (r0 / 2) < aa2
by A12, XXREAL_1:4;
A23:
pz in dom f1
by A19, FUNCT_2:def 1;
z in W1
by A17, XBOOLE_0:def 4;
then A24:
f1 . pz in f1 .: W1
by A23, FUNCT_1:def 6;
then
r1 - (r0 / 2) < aa1
by A14, XXREAL_1:4;
then
(r1 - (r0 / 2)) + (r2 - (r0 / 2)) < aa1 + aa2
by A22, XREAL_1:8;
then
(r1 + r2) - ((r0 / 2) + (r0 / 2)) < aa1 + aa2
;
then A25:
r - r0 < aa1 + aa2
by A4;
A26:
aa2 < r2 + (r0 / 2)
by A12, A21, XXREAL_1:4;
A27:
x = aa1 + aa2
by A4, A18;
then reconsider rx =
x as
Real ;
aa1 < r1 + (r0 / 2)
by A14, A24, XXREAL_1:4;
then
aa1 + aa2 < (r1 + (r0 / 2)) + (r2 + (r0 / 2))
by A26, XREAL_1:8;
then
aa1 + aa2 < (r1 + r2) + ((r0 / 2) + (r0 / 2))
;
then
rx < r + r0
by A4, A27;
hence
x in ].(r - r0),(r + r0).[
by A27, A25, XXREAL_1:4;
verum
end;
(
W1 /\ W2 is
open &
p in W1 /\ W2 )
by A13, A11, XBOOLE_0:def 4;
hence
ex
W being
Subset of
X st
(
p in W &
W is
open &
g0 .: W c= V )
by A6, A15, XBOOLE_1:1;
verum
end;
then A28:
g0 is continuous
by Th10;
for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g0 . p = r1 + r2
by A4;
hence
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds
g . p = r1 + r2 ) & g is continuous )
by A28; verum