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
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 not f1 | Z is bounded or not f2 | Z1 is bounded or (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous )
assume that
A3: f1 | X is uniformly_continuous and
A4: f2 | X1 is uniformly_continuous and
A5: f1 | Z is bounded and
A6: f2 | Z1 is bounded ; :: thesis: (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous
consider x1 being real number such that
A7: for r being set st r in Z /\ (dom f1) holds
abs (f1 . r) <= x1 by A5, RFUNCT_1:73;
consider x2 being real number such that
A8: for r being set st r in Z1 /\ (dom f2) holds
abs (f2 . r) <= x2 by A6, RFUNCT_1:73;
reconsider x1 = x1, x2 = x2 as Real by XREAL_0:def 1;
set M1 = (abs x1) + 1;
set M2 = (abs x2) + 1;
set M = max (((abs x1) + 1),((abs x2) + 1));

A9: 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)) ) )
A10: (abs x1) + 1 <= max (((abs x1) + 1),((abs x2) + 1)) by XXREAL_0:25;
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 A11: r in (X /\ Z) /\ (X1 /\ Z1) by XBOOLE_1:16;
then A12: r in X /\ Z by XBOOLE_0:def 4;
then A13: r in Z by XBOOLE_0:def 4;
r in X by A12, XBOOLE_0:def 4;
then r in Z /\ (dom f1) by A1, A13, XBOOLE_0:def 4;
then A14: abs (f1 . r) <= x1 by A7;
x1 + 0 < (abs x1) + 1 by ABSVALUE:4, XREAL_1:8;
then abs (f1 . r) < (abs x1) + 1 by A14, XXREAL_0:2;
hence abs (f1 . r) < max (((abs x1) + 1),((abs x2) + 1)) by A10, XXREAL_0:2; :: thesis: abs (f2 . r) < max (((abs x1) + 1),((abs x2) + 1))
A15: (abs x2) + 1 <= max (((abs x1) + 1),((abs x2) + 1)) by XXREAL_0:25;
A16: r in X1 /\ Z1 by A11, XBOOLE_0:def 4;
then A17: r in Z1 by XBOOLE_0:def 4;
r in X1 by A16, XBOOLE_0:def 4;
then r in Z1 /\ (dom f2) by A2, A17, XBOOLE_0:def 4;
then A18: abs (f2 . r) <= x2 by A8;
x2 + 0 < (abs x2) + 1 by ABSVALUE:4, XREAL_1:8;
then abs (f2 . r) < (abs x2) + 1 by A18, XXREAL_0:2;
hence abs (f2 . r) < max (((abs x1) + 1),((abs x2) + 1)) by A15, XXREAL_0:2; :: thesis: verum

end;

A19: 0 + 0 < (abs x2) + 1 by COMPLEX1:46, XREAL_1:8;
0 + 0 < (abs x1) + 1 by COMPLEX1:46, XREAL_1:8;
then A20: 0 < max (((abs x1) + 1),((abs x2) + 1)) by A19, XXREAL_0:16;
then A21: 0 < 2 * (max (((abs x1) + 1),((abs x2) + 1))) by XREAL_1:129;
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 A22: 0 < r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))) by A21, XREAL_1:139;
then consider s being Real such that
A23: 0 < s and
A24: 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 A3, Th1;
consider g being Real such that
A25: 0 < g and
A26: 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 A4, A22, Th1;
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 A23, A25, 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 that
A27: y1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) and
A28: y2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) ; :: thesis: ( not abs (y1 - y2) < p or abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) < r )
assume A29: abs (y1 - y2) < p ; :: thesis: abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) < r
A30: y2 in ((X /\ Z) /\ X1) /\ Z1 by A28, RELAT_1:57;
then A31: y2 in (X /\ Z) /\ (X1 /\ Z1) by XBOOLE_1:16;
then y2 in X /\ Z by XBOOLE_0:def 4;
then y2 in X by XBOOLE_0:def 4;
then A32: y2 in dom (f1 | X) by A1, RELAT_1:62;
A33: y1 in ((X /\ Z) /\ X1) /\ Z1 by A27, RELAT_1:57;
then A34: y1 in (X /\ Z) /\ (X1 /\ Z1) by XBOOLE_1:16;
then y1 in X /\ Z by XBOOLE_0:def 4;
then y1 in X by XBOOLE_0:def 4;
then A35: y1 in dom (f1 | X) by A1, RELAT_1:62;
y2 in X1 /\ Z1 by A31, XBOOLE_0:def 4;
then y2 in X1 by XBOOLE_0:def 4;
then A36: y2 in dom (f2 | X1) by A2, RELAT_1:62;
y1 in X1 /\ Z1 by A34, XBOOLE_0:def 4;
then y1 in X1 by XBOOLE_0:def 4;
then A37: y1 in dom (f2 | X1) by A2, RELAT_1:62;
p <= g by XXREAL_0:17;
then abs (y1 - y2) < g by A29, XXREAL_0:2;
then A38: abs ((f2 . y1) - (f2 . y2)) < r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))) by A26, A37, A36;
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 A39: abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= (abs ((f1 . y1) * ((f2 . y1) - (f2 . y2)))) + (abs (((f1 . y1) - (f1 . y2)) * (f2 . y2))) by COMPLEX1:56;
A40: abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) = (abs (f1 . y1)) * (abs ((f2 . y1) - (f2 . y2))) by COMPLEX1:65;
A41: abs (f2 . y2) < max (((abs x1) + 1),((abs x2) + 1)) by A9, A30;
A42: 0 <= abs (f2 . y2) by COMPLEX1:46;
A43: 0 <= abs ((f1 . y1) - (f1 . y2)) by COMPLEX1:46;
A44: abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) = (abs (f2 . y2)) * (abs ((f1 . y1) - (f1 . y2))) by COMPLEX1:65;
p <= s by XXREAL_0:17;
then abs (y1 - y2) < s by A29, XXREAL_0:2;
then abs ((f1 . y1) - (f1 . y2)) < r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))) by A24, A35, A32;
then A45: abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) < (max (((abs x1) + 1),((abs x2) + 1))) * (r / (2 * (max (((abs x1) + 1),((abs x2) + 1))))) by A44, A41, A43, A42, XREAL_1:96;
A46: 0 <= abs (f1 . y1) by COMPLEX1:46;
A47: 0 <= abs ((f2 . y1) - (f2 . y2)) by COMPLEX1:46;
abs (f1 . y1) < max (((abs x1) + 1),((abs x2) + 1)) by A9, A33;
then abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) < (max (((abs x1) + 1),((abs x2) + 1))) * (r / (2 * (max (((abs x1) + 1),((abs x2) + 1))))) by A40, A38, A47, A46, XREAL_1:96;
then A48: (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 A45, XREAL_1:8;
((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:118
.= r by A20, XCMPLX_1:87 ;
hence abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) < r by A39, A48, XXREAL_0:2; :: thesis: verum

end;

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