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 ;
then A10: |.(f2 . r).| <= x2 by A2;
x1 <= |.x1.| by ABSVALUE:4;
hence |.(f1 . r).| <= |.x1.| by ; :: thesis: |.(f2 . r).| <= |.x2.|
x2 <= |.x2.| by ABSVALUE:4;
hence |.(f2 . r).| <= |.x2.| by ; :: 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 ;
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 ;
then A16: |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| <= |.x1.| * |.((f2 . y1) - (f2 . y2)).| by ;
A17: y2 in dom f2 by ;
A18: y1 in (dom f1) /\ (dom f2) by ;
then y1 in dom f2 by XBOOLE_0:def 4;
then |.x1.| * |.((f2 . y1) - (f2 . y2)).| <= |.x1.| * (g * |.(y1 - y2).|) by ;
then A19: |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| <= (|.x1.| * g) * |.(y1 - y2).| by ;
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 ;
then A22: |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| <= |.x2.| * |.((f1 . y1) - (f1 . y2)).| by ;
A23: 0 <= |.x2.| by COMPLEX1:46;
y1 in dom f1 by ;
then |.x2.| * |.((f1 . y1) - (f1 . y2)).| <= |.x2.| * (s * |.(y1 - y2).|) by ;
then |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| <= |.x2.| * (s * |.(y1 - y2).|) by ;
then |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| + |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| <= ((|.x1.| * g) * |.(y1 - y2).|) + ((|.x2.| * s) * |.(y1 - y2).|) by ;
then |.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| <= ((|.x1.| * g) + (|.x2.| * s)) * |.(y1 - y2).| by ;
hence |.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| <= p * |.(y1 - y2).| by ; :: thesis: verum
end;
hence for b1 being PartFunc of REAL,REAL st b1 = f1 (#) f2 holds
b1 is Lipschitzian ; :: thesis: verum