set X = dom f1;
set X1 = dom f2;
consider s being real number such that
A9: ( 0 < s & ( for x1, x2 being real number st x1 in dom f1 & x2 in dom f1 holds
abs ((f1 . x1) - (f1 . x2)) <= s * (abs (x1 - x2)) ) ) by XDef3;
consider g being real number such that
A10: ( 0 < g & ( for x1, x2 being real number st x1 in dom f2 & x2 in dom f2 holds
abs ((f2 . x1) - (f2 . x2)) <= g * (abs (x1 - x2)) ) ) by XDef3;
consider x1 being real number such that
A11: for r being set st r in dom f1 holds
abs (f1 . r) <= x1 by RFUNCT_1:89;
consider x2 being real number such that
A12: for r being set st r in dom f2 holds
abs (f2 . r) <= x2 by RFUNCT_1:89;

A13: now

let r be real number ; :: thesis: ( r in dom (f1 (#) f2) implies ( abs (f1 . r) <= abs x1 & abs (f2 . r) <= abs x2 ) )
assume r in dom (f1 (#) f2) ; :: thesis: ( abs (f1 . r) <= abs x1 & abs (f2 . r) <= abs x2 )
then A14: r in (dom f1) /\ (dom f2) by VALUED_1:def 4;
then r in dom f1 by XBOOLE_0:def 4;
then A15: abs (f1 . r) <= x1 by A11;
x1 <= abs x1 by ABSVALUE:11;
hence abs (f1 . r) <= abs x1 by A15, XXREAL_0:2; :: thesis: abs (f2 . r) <= abs x2
r in dom f2 by A14, XBOOLE_0:def 4;
then A16: abs (f2 . r) <= x2 by A12;
x2 <= abs x2 by ABSVALUE:11;
hence abs (f2 . r) <= abs x2 by A16, XXREAL_0:2; :: thesis: verum

end;

now

take p = (((abs x1) * g) + ((abs x2) * s)) + 1; :: thesis: ( 0 < p & ( for y1, y2 being real number st y1 in dom (f1 (#) f2) & y2 in dom (f1 (#) f2) holds
abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= p * (abs (y1 - y2)) ) )
( 0 <= abs x1 & 0 <= abs x2 ) by COMPLEX1:132;
hence 0 < p by A9, A10; :: thesis: for y1, y2 being real number st y1 in dom (f1 (#) f2) & y2 in dom (f1 (#) f2) holds
abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= p * (abs (y1 - y2))
let y1, y2 be real number ; :: thesis: ( y1 in dom (f1 (#) f2) & y2 in dom (f1 (#) f2) implies abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= p * (abs (y1 - y2)) )
assume A19: ( y1 in dom (f1 (#) f2) & y2 in dom (f1 (#) f2) ) ; :: thesis: abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= p * (abs (y1 - y2))
then ( y1 in (dom f1) /\ (dom f2) & y2 in (dom f1) /\ (dom f2) ) by VALUED_1:def 4;
then A20: ( y1 in dom f1 & y1 in dom f2 & y2 in dom f1 & y2 in dom f2 ) by XBOOLE_0:def 4;
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 A21: abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= (abs ((f1 . y1) * ((f2 . y1) - (f2 . y2)))) + (abs (((f1 . y1) - (f1 . y2)) * (f2 . y2))) by COMPLEX1:142;
A22: abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) = (abs (f1 . y1)) * (abs ((f2 . y1) - (f2 . y2))) by COMPLEX1:151;
0 <= abs ((f2 . y1) - (f2 . y2)) by COMPLEX1:132;
then A24: abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) <= (abs x1) * (abs ((f2 . y1) - (f2 . y2))) by A22, A13, A19, XREAL_1:66;
0 <= abs x1 by COMPLEX1:132;
then (abs x1) * (abs ((f2 . y1) - (f2 . y2))) <= (abs x1) * (g * (abs (y1 - y2))) by A10, A20, XREAL_1:66;
then A25: abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) <= ((abs x1) * g) * (abs (y1 - y2)) by A24, XXREAL_0:2;
A26: abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) = (abs (f2 . y2)) * (abs ((f1 . y1) - (f1 . y2))) by COMPLEX1:151;
0 <= abs ((f1 . y1) - (f1 . y2)) by COMPLEX1:132;
then A28: abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) <= (abs x2) * (abs ((f1 . y1) - (f1 . y2))) by A26, A13, A19, XREAL_1:66;
0 <= abs x2 by COMPLEX1:132;
then (abs x2) * (abs ((f1 . y1) - (f1 . y2))) <= (abs x2) * (s * (abs (y1 - y2))) by A9, A20, XREAL_1:66;
then abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) <= (abs x2) * (s * (abs (y1 - y2))) by A28, XXREAL_0:2;
then (abs ((f1 . y1) * ((f2 . y1) - (f2 . y2)))) + (abs (((f1 . y1) - (f1 . y2)) * (f2 . y2))) <= (((abs x1) * g) * (abs (y1 - y2))) + (((abs x2) * s) * (abs (y1 - y2))) by A25, XREAL_1:9;
then A29: abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= (((abs x1) * g) + ((abs x2) * s)) * (abs (y1 - y2)) by A21, XXREAL_0:2;
0 <= abs (y1 - y2) by COMPLEX1:132;
then ((((abs x1) * g) + ((abs x2) * s)) * (abs (y1 - y2))) + 0 <= ((((abs x1) * g) + ((abs x2) * s)) * (abs (y1 - y2))) + (1 * (abs (y1 - y2))) by XREAL_1:9;
hence abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= p * (abs (y1 - y2)) by A29, XXREAL_0:2; :: thesis: verum

end;

hence for b₁ being PartFunc of REAL ,REAL st b₁ = f1 (#) f2 holds
b₁ is Lipschitzian by XDef3; :: thesis: verum