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
Z1: X c= dom f1 and
Z2: 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 )
assume A1: ( f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous ) ; :: thesis: (f1 + f2) | (X /\ X1) is uniformly_continuous
then A2: f1 | (X /\ X1) is uniformly_continuous by Th2, XBOOLE_1:17;
A3: X /\ X1 c= dom f1 by Z1, XBOOLE_1:108;
A4: f2 | (X /\ X1) is uniformly_continuous by A1, Th2, XBOOLE_1:17;
X /\ X1 c= dom f2 by Z2, XBOOLE_1:108;
then X /\ X1 c= (dom f1) /\ (dom f2) by A3, XBOOLE_1:19;
then A5: X /\ X1 c= dom (f1 + f2) by VALUED_1:def 1;

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 ) ) )
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 A6: 0 < r / 2 by XREAL_1:217;
then consider s being Real such that
A7: ( 0 < s & ( 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 A2, Def1;
consider g being Real such that
A8: ( 0 < g & ( 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 A4, A6, Def1;
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 A7, A8, 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
A9: ( p <= s & p <= g ) by XXREAL_0:17;
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 A10: ( x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & abs (x1 - x2) < p ) ; :: thesis: abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r
F0: dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def 1;
F: ( x1 in dom (f1 + f2) & x2 in dom (f1 + f2) ) by A10, RELAT_1:86;
then F1: ( x1 in dom f1 & x2 in dom f1 ) by F0, XBOOLE_0:def 4;
F2: ( x1 in dom f2 & x2 in dom f2 ) by F, F0, XBOOLE_0:def 4;
X: ( x1 in X /\ X1 & x2 in X /\ X1 & abs (x1 - x2) < s ) by A9, A10, RELAT_1:86, XXREAL_0:2;
then ( x1 in dom (f1 | (X /\ X1)) & x2 in dom (f1 | (X /\ X1)) ) by F1, RELAT_1:86;
then A11: abs ((f1 . x1) - (f1 . x2)) < r / 2 by A7, X;
Y: ( x1 in X /\ X1 & x2 in X /\ X1 & abs (x1 - x2) < g ) by A9, A10, X, XXREAL_0:2;
then ( x1 in dom (f2 | (X /\ X1)) & x2 in dom (f2 | (X /\ X1)) ) by F2, RELAT_1:86;
then abs ((f2 . x1) - (f2 . x2)) < r / 2 by A8, Y;
then A12: (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) < (r / 2) + (r / 2) by A11, XREAL_1:10;
A13: abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) = abs (((f1 . x1) + (f2 . x1)) - ((f1 + f2) . x2)) by A5, X, VALUED_1:def 1
.= abs (((f1 . x1) + (f2 . x1)) - ((f1 . x2) + (f2 . x2))) by A5, X, VALUED_1:def 1
.= abs (((f1 . x1) - (f1 . x2)) + ((f2 . x1) - (f2 . x2))) ;
abs (((f1 . x1) - (f1 . x2)) + ((f2 . x1) - (f2 . x2))) <= (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) by COMPLEX1:142;
hence abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r by A12, A13, XXREAL_0:2; :: thesis: verum

end;

hence (f1 + f2) | (X /\ X1) is uniformly_continuous by Def1; :: thesis: verum