set X = dom f1;
set X1 = dom f2;
consider x1 being Real such that
A1: for r being object st r in dom f1 holds
|.(f1 . r).| <= x1 by RFUNCT_1:72;
consider x2 being Real such that
A2: for r being object st r in dom f2 holds
|.(f2 . r).| <= x2 by RFUNCT_1:72;
consider g being Real such that
A3: 0 < g and
A4: for x1, x2 being Real st x1 in dom f2 & x2 in dom f2 holds
|.((f2 . x1) - (f2 . x2)).| <= g * |.(x1 - x2).| by Def3;
consider s being Real such that
A5: 0 < s and
A6: for x1, x2 being Real st x1 in dom f1 & x2 in dom f1 holds
|.((f1 . x1) - (f1 . x2)).| <= s * |.(x1 - x2).| by Def3;
A7: now :: thesis: for r being Real st r in dom (f1 (#) f2) holds
( |.(f1 . r).| <= |.x1.| & |.(f2 . r).| <= |.x2.| )
let r be Real; :: thesis: ( r in dom (f1 (#) f2) implies ( |.(f1 . r).| <= |.x1.| & |.(f2 . r).| <= |.x2.| ) )
assume r in dom (f1 (#) f2) ; :: thesis: ( |.(f1 . r).| <= |.x1.| & |.(f2 . r).| <= |.x2.| )
then A8: r in (dom f1) /\ (dom f2) by VALUED_1:def 4;
then r in dom f1 by XBOOLE_0:def 4;
then A9: |.(f1 . r).| <= x1 by A1;
r in dom f2 by A8, XBOOLE_0:def 4;
then A10: |.(f2 . r).| <= x2 by A2;
x1 <= |.x1.| by ABSVALUE:4;
hence |.(f1 . r).| <= |.x1.| by A9, XXREAL_0:2; :: thesis: |.(f2 . r).| <= |.x2.|
x2 <= |.x2.| by ABSVALUE:4;
hence |.(f2 . r).| <= |.x2.| by A10, XXREAL_0:2; :: thesis: verum
end;
now :: thesis: ex p being set st
( 0 < p & ( for y1, y2 being Real st y1 in dom (f1 (#) f2) & y2 in dom (f1 (#) f2) holds
|.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| <= p * |.(y1 - y2).| ) )
take p = ((|.x1.| * g) + (|.x2.| * s)) + 1; :: thesis: ( 0 < p & ( for y1, y2 being Real st y1 in dom (f1 (#) f2) & y2 in dom (f1 (#) f2) holds
|.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| <= p * |.(y1 - y2).| ) )
A11: 0 <= |.x1.| by COMPLEX1:46;
( 0 <= |.x1.| & 0 <= |.x2.| ) by COMPLEX1:46;
hence 0 < p by A5, A3; :: thesis: for y1, y2 being Real st y1 in dom (f1 (#) f2) & y2 in dom (f1 (#) f2) holds
|.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| <= p * |.(y1 - y2).|
let y1, y2 be Real; :: thesis: ( y1 in dom (f1 (#) f2) & y2 in dom (f1 (#) f2) implies |.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| <= p * |.(y1 - y2).| )
assume that
A12: y1 in dom (f1 (#) f2) and
A13: y2 in dom (f1 (#) f2) ; :: thesis: |.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| <= p * |.(y1 - y2).|
A14: y2 in (dom f1) /\ (dom f2) by A13, VALUED_1:def 4;
then A15: y2 in dom f1 by XBOOLE_0:def 4;
( |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| = |.(f1 . y1).| * |.((f2 . y1) - (f2 . y2)).| & 0 <= |.((f2 . y1) - (f2 . y2)).| ) by COMPLEX1:46, COMPLEX1:65;
then A16: |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| <= |.x1.| * |.((f2 . y1) - (f2 . y2)).| by A7, A12, XREAL_1:64;
A17: y2 in dom f2 by A14, XBOOLE_0:def 4;
A18: y1 in (dom f1) /\ (dom f2) by A12, VALUED_1:def 4;
then y1 in dom f2 by XBOOLE_0:def 4;
then |.x1.| * |.((f2 . y1) - (f2 . y2)).| <= |.x1.| * (g * |.(y1 - y2).|) by A4, A17, A11, XREAL_1:64;
then A19: |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| <= (|.x1.| * g) * |.(y1 - y2).| by A16, XXREAL_0:2;
0 <= |.(y1 - y2).| by COMPLEX1:46;
then A20: (((|.x1.| * g) + (|.x2.| * s)) * |.(y1 - y2).|) + 0 <= (((|.x1.| * g) + (|.x2.| * s)) * |.(y1 - y2).|) + (1 * |.(y1 - y2).|) by XREAL_1:7;
|.(((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 A21: |.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| <= |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| + |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| by COMPLEX1:56;
( |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| = |.(f2 . y2).| * |.((f1 . y1) - (f1 . y2)).| & 0 <= |.((f1 . y1) - (f1 . y2)).| ) by COMPLEX1:46, COMPLEX1:65;
then A22: |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| <= |.x2.| * |.((f1 . y1) - (f1 . y2)).| by A7, A13, XREAL_1:64;
A23: 0 <= |.x2.| by COMPLEX1:46;
y1 in dom f1 by A18, XBOOLE_0:def 4;
then |.x2.| * |.((f1 . y1) - (f1 . y2)).| <= |.x2.| * (s * |.(y1 - y2).|) by A6, A15, A23, XREAL_1:64;
then |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| <= |.x2.| * (s * |.(y1 - y2).|) by A22, XXREAL_0:2;
then |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| + |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| <= ((|.x1.| * g) * |.(y1 - y2).|) + ((|.x2.| * s) * |.(y1 - y2).|) by A19, XREAL_1:7;
then |.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| <= ((|.x1.| * g) + (|.x2.| * s)) * |.(y1 - y2).| by A21, XXREAL_0:2;
hence |.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| <= p * |.(y1 - y2).| by A20, XXREAL_0:2; :: thesis: verum
end;
hence for b1 being PartFunc of REAL,REAL st b1 = f1 (#) f2 holds
b1 is Lipschitzian ; :: thesis: verum