let X, X1 be set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: (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 :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( 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; :: thesis: 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 x1, x2 be Real; :: thesis: ( 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 ; :: thesis: |.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| < r
A18: 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; :: thesis: verum
end;
hence (f1 + f2) | (X /\ X1) is uniformly_continuous by Th1; :: thesis: verum