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

let r be Real; :: thesis: ( 0 < r implies ex p being Element of REAL st
( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & abs (x1 - x2) < p holds
abs (((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 Element of REAL st
( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & abs (x1 - x2) < p holds
abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r ) )
then A10: 0 < r / 2 by XREAL_1:217;
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)) & abs (x1 - x2) < s holds
abs ((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)) & abs (x1 - x2) < g holds
abs ((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)) & abs (x1 - x2) < p holds
abs (((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)) & abs (x1 - x2) < p holds
abs (((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)) & abs (x1 - x2) < p implies abs (((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: abs (x1 - x2) < p ; :: thesis: abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r
A18: x2 in X /\ X1 by A16, RELAT_1:86;
A19: x2 in dom (f1 + f2) by A16, RELAT_1:86;
then x2 in dom f2 by A9, XBOOLE_0:def 4;
then A20: x2 in dom (f2 | (X /\ X1)) by A18, RELAT_1:86;
p <= g by XXREAL_0:17;
then A21: abs (x1 - x2) < g by A17, XXREAL_0:2;
A22: x1 in X /\ X1 by A15, RELAT_1:86;
x2 in dom f1 by A9, A19, XBOOLE_0:def 4;
then A23: x2 in dom (f1 | (X /\ X1)) by A18, RELAT_1:86;
p <= s by XXREAL_0:17;
then A24: abs (x1 - x2) < s by A17, XXREAL_0:2;
A25: x1 in dom (f1 + f2) by A15, RELAT_1:86;
then x1 in dom f2 by A9, XBOOLE_0:def 4;
then x1 in dom (f2 | (X /\ X1)) by A22, RELAT_1:86;
then A26: abs ((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:86;
then abs ((f1 . x1) - (f1 . x2)) < r / 2 by A12, A24, A23;
then A27: (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) < (r / 2) + (r / 2) by A26, XREAL_1:10;
A28: abs (((f1 . x1) - (f1 . x2)) + ((f2 . x1) - (f2 . x2))) <= (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) by COMPLEX1:142;
abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) = abs (((f1 . x1) + (f2 . x1)) - ((f1 + f2) . x2)) by A4, A22, VALUED_1:def 1
.= abs (((f1 . x1) + (f2 . x1)) - ((f1 . x2) + (f2 . x2))) by A4, A18, VALUED_1:def 1
.= abs (((f1 . x1) - (f1 . x2)) + ((f2 . x1) - (f2 . x2))) ;
hence abs (((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