set X = dom f1;
set X1 = dom f2;
consider x1 being real number such that
A1: 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
A2: for r being set st r in dom f2 holds
abs (f2 . r) <= x2 by RFUNCT_1:89;
consider g being real number such that
A3: 0 < g and
A4: 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 Def3;
consider s being real number such that
A5: 0 < s and
A6: 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 Def3;

A7: 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 A8: r in (dom f1) /\ (dom f2) by VALUED_1:def 4;
then r in dom f1 by XBOOLE_0:def 4;
then A9: abs (f1 . r) <= x1 by A1;
r in dom f2 by A8, XBOOLE_0:def 4;
then A10: abs (f2 . r) <= x2 by A2;
x1 <= abs x1 by ABSVALUE:11;
hence abs (f1 . r) <= abs x1 by A9, XXREAL_0:2; :: thesis: abs (f2 . r) <= abs x2
x2 <= abs x2 by ABSVALUE:11;
hence abs (f2 . r) <= abs x2 by A10, 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)) ) )
A11: 0 <= abs x1 by COMPLEX1:132;
( 0 <= abs x1 & 0 <= abs x2 ) by COMPLEX1:132;
hence 0 < p by A5, A3; :: 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 that
A12: y1 in dom (f1 (#) f2) and
A13: y2 in dom (f1 (#) f2) ; :: thesis: abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= p * (abs (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;
( abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) = (abs (f1 . y1)) * (abs ((f2 . y1) - (f2 . y2))) & 0 <= abs ((f2 . y1) - (f2 . y2)) ) by COMPLEX1:132, COMPLEX1:151;
then A16: abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) <= (abs x1) * (abs ((f2 . y1) - (f2 . y2))) by A7, A12, XREAL_1:66;
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 (abs x1) * (abs ((f2 . y1) - (f2 . y2))) <= (abs x1) * (g * (abs (y1 - y2))) by A4, A17, A11, XREAL_1:66;
then A19: abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) <= ((abs x1) * g) * (abs (y1 - y2)) by A16, XXREAL_0:2;
0 <= abs (y1 - y2) by COMPLEX1:132;
then A20: ((((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;
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;
( abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) = (abs (f2 . y2)) * (abs ((f1 . y1) - (f1 . y2))) & 0 <= abs ((f1 . y1) - (f1 . y2)) ) by COMPLEX1:132, COMPLEX1:151;
then A22: abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) <= (abs x2) * (abs ((f1 . y1) - (f1 . y2))) by A7, A13, XREAL_1:66;
A23: 0 <= abs x2 by COMPLEX1:132;
y1 in dom f1 by A18, XBOOLE_0:def 4;
then (abs x2) * (abs ((f1 . y1) - (f1 . y2))) <= (abs x2) * (s * (abs (y1 - y2))) by A6, A15, A23, XREAL_1:66;
then abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) <= (abs x2) * (s * (abs (y1 - y2))) by A22, 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 A19, XREAL_1:9;
then abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= (((abs x1) * g) + ((abs x2) * s)) * (abs (y1 - y2)) by A21, XXREAL_0:2;
hence abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= p * (abs (y1 - y2)) by A20, XXREAL_0:2; :: thesis: verum

end;

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