let X, X1, Z, Z1 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 & f1 | Z is bounded & f2 | Z1 is bounded holds
(f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) 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 & f1 | Z is bounded & f2 | Z1 is bounded implies (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) 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 not f1 | Z is bounded or not f2 | Z1 is bounded or (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous )
assume that
A1: f1 | X is uniformly_continuous and
A2: f2 | X1 is uniformly_continuous and
A3: f1 | Z is bounded and
A4: f2 | Z1 is bounded ; :: thesis: (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous
A5: X c= dom f1 by Z1;
A6: X1 c= dom f2 by Z2;
consider x1 being real number such that
A9: for r being set st r in Z /\ (dom f1) holds
abs (f1 . r) <= x1 by A3, RFUNCT_1:90;
consider x2 being real number such that
A10: for r being set st r in Z1 /\ (dom f2) holds
abs (f2 . r) <= x2 by A4, RFUNCT_1:90;
reconsider x1 = x1, x2 = x2 as Real by XREAL_0:def 1;
A11: 0 + 0 < (abs x1) + 1 by COMPLEX1:132, XREAL_1:10;
A12: 0 + 0 < (abs x2) + 1 by COMPLEX1:132, XREAL_1:10;
set M1 = (abs x1) + 1;
set M2 = (abs x2) + 1;
set M = max ((abs x1) + 1),((abs x2) + 1);

A13: now

let r be Real; :: thesis: ( r in ((X /\ Z) /\ X1) /\ Z1 implies ( abs (f1 . r) < max ((abs x1) + 1),((abs x2) + 1) & abs (f2 . r) < max ((abs x1) + 1),((abs x2) + 1) ) )
assume r in ((X /\ Z) /\ X1) /\ Z1 ; :: thesis: ( abs (f1 . r) < max ((abs x1) + 1),((abs x2) + 1) & abs (f2 . r) < max ((abs x1) + 1),((abs x2) + 1) )
then A14: r in (X /\ Z) /\ (X1 /\ Z1) by XBOOLE_1:16;
then r in X /\ Z by XBOOLE_0:def 4;
then ( r in X & r in Z ) by XBOOLE_0:def 4;
then r in Z /\ (dom f1) by A5, XBOOLE_0:def 4;
then A15: abs (f1 . r) <= x1 by A9;
x1 + 0 < (abs x1) + 1 by ABSVALUE:11, XREAL_1:10;
then A16: abs (f1 . r) < (abs x1) + 1 by A15, XXREAL_0:2;
(abs x1) + 1 <= max ((abs x1) + 1),((abs x2) + 1) by XXREAL_0:25;
hence abs (f1 . r) < max ((abs x1) + 1),((abs x2) + 1) by A16, XXREAL_0:2; :: thesis: abs (f2 . r) < max ((abs x1) + 1),((abs x2) + 1)
r in X1 /\ Z1 by A14, XBOOLE_0:def 4;
then ( r in X1 & r in Z1 ) by XBOOLE_0:def 4;
then r in Z1 /\ (dom f2) by A6, XBOOLE_0:def 4;
then A17: abs (f2 . r) <= x2 by A10;
x2 + 0 < (abs x2) + 1 by ABSVALUE:11, XREAL_1:10;
then A18: abs (f2 . r) < (abs x2) + 1 by A17, XXREAL_0:2;
(abs x2) + 1 <= max ((abs x1) + 1),((abs x2) + 1) by XXREAL_0:25;
hence abs (f2 . r) < max ((abs x1) + 1),((abs x2) + 1) by A18, XXREAL_0:2; :: thesis: verum

end;

A19: 0 < max ((abs x1) + 1),((abs x2) + 1) by A11, A12, XXREAL_0:16;
then A20: 0 < 2 * (max ((abs x1) + 1),((abs x2) + 1)) by XREAL_1:131;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & x2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (x1 - x2) < s holds
abs (((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)) < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & x2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (x1 - x2) < s holds
abs (((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)) < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & x2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (x1 - x2) < s holds
abs (((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)) < r ) )
then A21: 0 < r / (2 * (max ((abs x1) + 1),((abs x2) + 1))) by A20, XREAL_1:141;
then consider s being Real such that
A22: ( 0 < s & ( for x1, x2 being Real st x1 in dom (f1 | X) & x2 in dom (f1 | X) & abs (x1 - x2) < s holds
abs ((f1 . x1) - (f1 . x2)) < r / (2 * (max ((abs x1) + 1),((abs x2) + 1))) ) ) by A1, Def1;
consider g being Real such that
A23: ( 0 < g & ( for x1, x2 being Real st x1 in dom (f2 | X1) & x2 in dom (f2 | X1) & abs (x1 - x2) < g holds
abs ((f2 . x1) - (f2 . x2)) < r / (2 * (max ((abs x1) + 1),((abs x2) + 1))) ) ) by A2, A21, Def1;
take p = min s,g; :: thesis: ( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & x2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (x1 - x2) < p holds
abs (((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)) < r ) )
thus 0 < p by A22, A23, XXREAL_0:15; :: thesis: for x1, x2 being Real st x1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & x2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (x1 - x2) < p holds
abs (((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)) < r
let y1, y2 be Real; :: thesis: ( y1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & y2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (y1 - y2) < p implies abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) < r )
assume ( y1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & y2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) ) ; :: thesis: ( not abs (y1 - y2) < p or abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) < r )
then A24: ( y1 in ((X /\ Z) /\ X1) /\ Z1 & y2 in ((X /\ Z) /\ X1) /\ Z1 ) by RELAT_1:86;
assume Z: abs (y1 - y2) < p ; :: thesis: abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) < r
( y1 in (X /\ Z) /\ (X1 /\ Z1) & y2 in (X /\ Z) /\ (X1 /\ Z1) ) by A24, XBOOLE_1:16;
then ( y1 in X /\ Z & y1 in X1 /\ Z1 & y2 in X /\ Z & y2 in X1 /\ Z1 ) by XBOOLE_0:def 4;
then A25: ( y1 in X & y1 in X1 & y2 in X & y2 in X1 ) by XBOOLE_0:def 4;
( p <= s & p <= g ) by XXREAL_0:17;
then A26: ( abs (y1 - y2) < s & abs (y1 - y2) < g ) by Z, XXREAL_0:2;
abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) = abs (((f1 . y1) * (f2 . y1)) - ((f1 (#) f2) . y2)) by VALUED_1:5
.= abs ((((f1 . y1) * (f2 . y1)) + (((f1 . y1) * (f2 . y2)) - ((f1 . y1) * (f2 . y2)))) - ((f1 . y2) * (f2 . y2))) by VALUED_1:5
.= abs (((f1 . y1) * ((f2 . y1) - (f2 . y2))) + (((f1 . y1) - (f1 . y2)) * (f2 . y2))) ;
then A27: abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= (abs ((f1 . y1) * ((f2 . y1) - (f2 . y2)))) + (abs (((f1 . y1) - (f1 . y2)) * (f2 . y2))) by COMPLEX1:142;
A28: abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) = (abs (f1 . y1)) * (abs ((f2 . y1) - (f2 . y2))) by COMPLEX1:151;
( y1 in dom (f2 | X1) & y2 in dom (f2 | X1) ) by A25, Z2, RELAT_1:91;
then A29: abs ((f2 . y1) - (f2 . y2)) < r / (2 * (max ((abs x1) + 1),((abs x2) + 1))) by A23, A26;
A30: abs (f1 . y1) < max ((abs x1) + 1),((abs x2) + 1) by A13, A24;
A31: 0 <= abs ((f2 . y1) - (f2 . y2)) by COMPLEX1:132;
0 <= abs (f1 . y1) by COMPLEX1:132;
then A32: abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) < (max ((abs x1) + 1),((abs x2) + 1)) * (r / (2 * (max ((abs x1) + 1),((abs x2) + 1)))) by A28, A29, A30, A31, XREAL_1:98;
A33: abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) = (abs (f2 . y2)) * (abs ((f1 . y1) - (f1 . y2))) by COMPLEX1:151;
( y1 in dom (f1 | X) & y2 in dom (f1 | X) ) by A25, Z1, RELAT_1:91;
then A34: abs ((f1 . y1) - (f1 . y2)) < r / (2 * (max ((abs x1) + 1),((abs x2) + 1))) by A22, A26;
A35: abs (f2 . y2) < max ((abs x1) + 1),((abs x2) + 1) by A13, A24;
A36: 0 <= abs ((f1 . y1) - (f1 . y2)) by COMPLEX1:132;
0 <= abs (f2 . y2) by COMPLEX1:132;
then abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) < (max ((abs x1) + 1),((abs x2) + 1)) * (r / (2 * (max ((abs x1) + 1),((abs x2) + 1)))) by A33, A34, A35, A36, XREAL_1:98;
then A37: (abs ((f1 . y1) * ((f2 . y1) - (f2 . y2)))) + (abs (((f1 . y1) - (f1 . y2)) * (f2 . y2))) < ((max ((abs x1) + 1),((abs x2) + 1)) * (r / (2 * (max ((abs x1) + 1),((abs x2) + 1))))) + ((max ((abs x1) + 1),((abs x2) + 1)) * (r / (2 * (max ((abs x1) + 1),((abs x2) + 1))))) by A32, XREAL_1:10;
((max ((abs x1) + 1),((abs x2) + 1)) * (r / (2 * (max ((abs x1) + 1),((abs x2) + 1))))) + ((max ((abs x1) + 1),((abs x2) + 1)) * (r / (2 * (max ((abs x1) + 1),((abs x2) + 1))))) = (max ((abs x1) + 1),((abs x2) + 1)) * ((r / ((max ((abs x1) + 1),((abs x2) + 1)) * 2)) + (r / ((max ((abs x1) + 1),((abs x2) + 1)) * 2)))
.= (r / (max ((abs x1) + 1),((abs x2) + 1))) * (max ((abs x1) + 1),((abs x2) + 1)) by XCMPLX_1:119
.= r by A19, XCMPLX_1:88 ;
hence abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) < r by A27, A37, XXREAL_0:2; :: thesis: verum

end;

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