let X, X1 be set ; for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous holds
(f1 + f2) | (X /\ X1) is uniformly_continuous
let f1, f2 be PartFunc of REAL,REAL; ( X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous implies (f1 + f2) | (X /\ X1) is uniformly_continuous )
assume that
A1:
X c= dom f1
and
A2:
X1 c= dom f2
; ( not f1 | X is uniformly_continuous or not f2 | X1 is uniformly_continuous or (f1 + f2) | (X /\ X1) is uniformly_continuous )
A3:
X /\ X1 c= dom f2
by A2, XBOOLE_1:108;
X /\ X1 c= dom f1
by A1, XBOOLE_1:108;
then
X /\ X1 c= (dom f1) /\ (dom f2)
by A3, XBOOLE_1:19;
then A4:
X /\ X1 c= dom (f1 + f2)
by VALUED_1:def 1;
assume that
A5:
f1 | X is uniformly_continuous
and
A6:
f2 | X1 is uniformly_continuous
; (f1 + f2) | (X /\ X1) is uniformly_continuous
A7:
f2 | (X /\ X1) is uniformly_continuous
by A6, Th2, XBOOLE_1:17;
A8:
f1 | (X /\ X1) is uniformly_continuous
by A5, Th2, XBOOLE_1:17;
now for r being Real st 0 < r holds
ex p being object st
( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & |.(x1 - x2).| < p holds
|.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| < r ) )let r be
Real;
( 0 < r implies ex p being object st
( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & |.(x1 - x2).| < p holds
|.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| < r ) ) )A9:
dom (f1 + f2) = (dom f1) /\ (dom f2)
by VALUED_1:def 1;
assume
0 < r
;
ex p being object st
( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & |.(x1 - x2).| < p holds
|.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| < r ) )then A10:
0 < r / 2
by XREAL_1:215;
then consider s being
Real such that A11:
0 < s
and A12:
for
x1,
x2 being
Real st
x1 in dom (f1 | (X /\ X1)) &
x2 in dom (f1 | (X /\ X1)) &
|.(x1 - x2).| < s holds
|.((f1 . x1) - (f1 . x2)).| < r / 2
by A8, Th1;
consider g being
Real such that A13:
0 < g
and A14:
for
x1,
x2 being
Real st
x1 in dom (f2 | (X /\ X1)) &
x2 in dom (f2 | (X /\ X1)) &
|.(x1 - x2).| < g holds
|.((f2 . x1) - (f2 . x2)).| < r / 2
by A7, A10, Th1;
take p =
min (
s,
g);
( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & |.(x1 - x2).| < p holds
|.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| < r ) )thus
0 < p
by A11, A13, XXREAL_0:15;
for x1, x2 being Real st x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & |.(x1 - x2).| < p holds
|.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| < rlet x1,
x2 be
Real;
( x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & |.(x1 - x2).| < p implies |.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| < r )assume that A15:
x1 in dom ((f1 + f2) | (X /\ X1))
and A16:
x2 in dom ((f1 + f2) | (X /\ X1))
and A17:
|.(x1 - x2).| < p
;
|.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| < rA18:
x2 in X /\ X1
by A16, RELAT_1:57;
A19:
x2 in dom (f1 + f2)
by A16, RELAT_1:57;
then
x2 in dom f2
by A9, XBOOLE_0:def 4;
then A20:
x2 in dom (f2 | (X /\ X1))
by A18, RELAT_1:57;
p <= g
by XXREAL_0:17;
then A21:
|.(x1 - x2).| < g
by A17, XXREAL_0:2;
A22:
x1 in X /\ X1
by A15, RELAT_1:57;
x2 in dom f1
by A9, A19, XBOOLE_0:def 4;
then A23:
x2 in dom (f1 | (X /\ X1))
by A18, RELAT_1:57;
p <= s
by XXREAL_0:17;
then A24:
|.(x1 - x2).| < s
by A17, XXREAL_0:2;
A25:
x1 in dom (f1 + f2)
by A15, RELAT_1:57;
then
x1 in dom f2
by A9, XBOOLE_0:def 4;
then
x1 in dom (f2 | (X /\ X1))
by A22, RELAT_1:57;
then A26:
|.((f2 . x1) - (f2 . x2)).| < r / 2
by A14, A21, A20;
x1 in dom f1
by A9, A25, XBOOLE_0:def 4;
then
x1 in dom (f1 | (X /\ X1))
by A22, RELAT_1:57;
then
|.((f1 . x1) - (f1 . x2)).| < r / 2
by A12, A24, A23;
then A27:
|.((f1 . x1) - (f1 . x2)).| + |.((f2 . x1) - (f2 . x2)).| < (r / 2) + (r / 2)
by A26, XREAL_1:8;
A28:
|.(((f1 . x1) - (f1 . x2)) + ((f2 . x1) - (f2 . x2))).| <= |.((f1 . x1) - (f1 . x2)).| + |.((f2 . x1) - (f2 . x2)).|
by COMPLEX1:56;
|.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| =
|.(((f1 . x1) + (f2 . x1)) - ((f1 + f2) . x2)).|
by A4, A22, VALUED_1:def 1
.=
|.(((f1 . x1) + (f2 . x1)) - ((f1 . x2) + (f2 . x2))).|
by A4, A18, VALUED_1:def 1
.=
|.(((f1 . x1) - (f1 . x2)) + ((f2 . x1) - (f2 . x2))).|
;
hence
|.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| < r
by A27, A28, XXREAL_0:2;
verum end;
hence
(f1 + f2) | (X /\ X1) is uniformly_continuous
by Th1; verum