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 such that
A7: for r being object st r in Z /\ (dom f1) holds
|.(f1 . r).| <= x1 by A5, RFUNCT_1:73;
consider x2 being Real such that
A8: for r being object st r in Z1 /\ (dom f2) holds
|.(f2 . r).| <= x2 by A6, RFUNCT_1:73;
reconsider x1 = x1, x2 = x2 as Real ;
set M1 = |.x1.| + 1;
set M2 = |.x2.| + 1;
set M = max ((|.x1.| + 1),(|.x2.| + 1));
A9: now :: thesis: for r being Real st r in ((X /\ Z) /\ X1) /\ Z1 holds
( |.(f1 . r).| < max ((|.x1.| + 1),(|.x2.| + 1)) & |.(f2 . r).| < max ((|.x1.| + 1),(|.x2.| + 1)) )
let r be Real; :: thesis: ( r in ((X /\ Z) /\ X1) /\ Z1 implies ( |.(f1 . r).| < max ((|.x1.| + 1),(|.x2.| + 1)) & |.(f2 . r).| < max ((|.x1.| + 1),(|.x2.| + 1)) ) )
A10: |.x1.| + 1 <= max ((|.x1.| + 1),(|.x2.| + 1)) by XXREAL_0:25;
assume r in ((X /\ Z) /\ X1) /\ Z1 ; :: thesis: ( |.(f1 . r).| < max ((|.x1.| + 1),(|.x2.| + 1)) & |.(f2 . r).| < max ((|.x1.| + 1),(|.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: |.(f1 . r).| <= x1 by A7;
x1 + 0 < |.x1.| + 1 by ABSVALUE:4, XREAL_1:8;
then |.(f1 . r).| < |.x1.| + 1 by A14, XXREAL_0:2;
hence |.(f1 . r).| < max ((|.x1.| + 1),(|.x2.| + 1)) by A10, XXREAL_0:2; :: thesis: |.(f2 . r).| < max ((|.x1.| + 1),(|.x2.| + 1))
A15: |.x2.| + 1 <= max ((|.x1.| + 1),(|.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: |.(f2 . r).| <= x2 by A8;
x2 + 0 < |.x2.| + 1 by ABSVALUE:4, XREAL_1:8;
then |.(f2 . r).| < |.x2.| + 1 by A18, XXREAL_0:2;
hence |.(f2 . r).| < max ((|.x1.| + 1),(|.x2.| + 1)) by A15, XXREAL_0:2; :: thesis: verum
end;
A19: 0 + 0 < |.x2.| + 1 by COMPLEX1:46, XREAL_1:8;
0 + 0 < |.x1.| + 1 by COMPLEX1:46, XREAL_1:8;
then A20: 0 < max ((|.x1.| + 1),(|.x2.| + 1)) by A19, XXREAL_0:16;
then A21: 0 < 2 * (max ((|.x1.| + 1),(|.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)) & |.(x1 - x2).| < s holds
|.(((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)) & |.(x1 - x2).| < s holds
|.(((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)) & |.(x1 - x2).| < s holds
|.(((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)).| < r ) )
then A22: 0 < r / (2 * (max ((|.x1.| + 1),(|.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) & |.(x1 - x2).| < s holds
|.((f1 . x1) - (f1 . x2)).| < r / (2 * (max ((|.x1.| + 1),(|.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) & |.(x1 - x2).| < g holds
|.((f2 . x1) - (f2 . x2)).| < r / (2 * (max ((|.x1.| + 1),(|.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)) & |.(x1 - x2).| < p holds
|.(((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)) & |.(x1 - x2).| < p holds
|.(((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)) & |.(y1 - y2).| < p implies |.(((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 |.(y1 - y2).| < p or |.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| < r )
assume A29: |.(y1 - y2).| < p ; :: thesis: |.(((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 |.(y1 - y2).| < g by A29, XXREAL_0:2;
then A38: |.((f2 . y1) - (f2 . y2)).| < r / (2 * (max ((|.x1.| + 1),(|.x2.| + 1)))) by A26, A37, A36;
|.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| = |.(((f1 . y1) * (f2 . y1)) - ((f1 (#) f2) . y2)).| by VALUED_1:5
.= |.((((f1 . y1) * (f2 . y1)) + (((f1 . y1) * (f2 . y2)) - ((f1 . y1) * (f2 . y2)))) - ((f1 . y2) * (f2 . y2))).| by VALUED_1:5
.= |.(((f1 . y1) * ((f2 . y1) - (f2 . y2))) + (((f1 . y1) - (f1 . y2)) * (f2 . y2))).| ;
then A39: |.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| <= |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| + |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| by COMPLEX1:56;
A40: |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| = |.(f1 . y1).| * |.((f2 . y1) - (f2 . y2)).| by COMPLEX1:65;
A41: |.(f2 . y2).| < max ((|.x1.| + 1),(|.x2.| + 1)) by A9, A30;
A42: 0 <= |.(f2 . y2).| by COMPLEX1:46;
A43: 0 <= |.((f1 . y1) - (f1 . y2)).| by COMPLEX1:46;
A44: |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| = |.(f2 . y2).| * |.((f1 . y1) - (f1 . y2)).| by COMPLEX1:65;
p <= s by XXREAL_0:17;
then |.(y1 - y2).| < s by A29, XXREAL_0:2;
then |.((f1 . y1) - (f1 . y2)).| < r / (2 * (max ((|.x1.| + 1),(|.x2.| + 1)))) by A24, A35, A32;
then A45: |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| < (max ((|.x1.| + 1),(|.x2.| + 1))) * (r / (2 * (max ((|.x1.| + 1),(|.x2.| + 1))))) by A44, A41, A43, A42, XREAL_1:96;
A46: 0 <= |.(f1 . y1).| by COMPLEX1:46;
A47: 0 <= |.((f2 . y1) - (f2 . y2)).| by COMPLEX1:46;
|.(f1 . y1).| < max ((|.x1.| + 1),(|.x2.| + 1)) by A9, A33;
then |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| < (max ((|.x1.| + 1),(|.x2.| + 1))) * (r / (2 * (max ((|.x1.| + 1),(|.x2.| + 1))))) by A40, A38, A47, A46, XREAL_1:96;
then A48: |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| + |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| < ((max ((|.x1.| + 1),(|.x2.| + 1))) * (r / (2 * (max ((|.x1.| + 1),(|.x2.| + 1)))))) + ((max ((|.x1.| + 1),(|.x2.| + 1))) * (r / (2 * (max ((|.x1.| + 1),(|.x2.| + 1)))))) by A45, XREAL_1:8;
((max ((|.x1.| + 1),(|.x2.| + 1))) * (r / (2 * (max ((|.x1.| + 1),(|.x2.| + 1)))))) + ((max ((|.x1.| + 1),(|.x2.| + 1))) * (r / (2 * (max ((|.x1.| + 1),(|.x2.| + 1)))))) = (max ((|.x1.| + 1),(|.x2.| + 1))) * ((r / ((max ((|.x1.| + 1),(|.x2.| + 1))) * 2)) + (r / ((max ((|.x1.| + 1),(|.x2.| + 1))) * 2)))
.= (r / (max ((|.x1.| + 1),(|.x2.| + 1)))) * (max ((|.x1.| + 1),(|.x2.| + 1))) by XCMPLX_1:118
.= r by A20, XCMPLX_1:87 ;
hence |.(((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