set X = dom f1;
set X1 = dom f2;
consider s being Real such that
A9: 0 < s and
A10: for x1, x2 being Real st x1 in dom (f1 | ((dom f1) /\ (dom f2))) & x2 in dom (f1 | ((dom f1) /\ (dom f2))) holds
|.((f1 . x1) - (f1 . x2)).| <= s * |.(x1 - x2).| by Th32;
consider g being Real such that
A11: 0 < g and
A12: for x1, x2 being Real st x1 in dom (f2 | ((dom f1) /\ (dom f2))) & x2 in dom (f2 | ((dom f1) /\ (dom f2))) holds
|.((f2 . x1) - (f2 . x2)).| <= g * |.(x1 - x2).| by Th32;
now :: thesis: ex p being set st
( 0 < p & ( for x1, x2 being Real st x1 in dom (f1 - f2) & x2 in dom (f1 - f2) holds
|.(((f1 - f2) . x1) - ((f1 - f2) . x2)).| <= p * |.(x1 - x2).| ) )
take p = s + g; :: thesis: ( 0 < p & ( for x1, x2 being Real st x1 in dom (f1 - f2) & x2 in dom (f1 - f2) holds
|.(((f1 - f2) . x1) - ((f1 - f2) . x2)).| <= p * |.(x1 - x2).| ) )

thus 0 < p by ; :: thesis: for x1, x2 being Real st x1 in dom (f1 - f2) & x2 in dom (f1 - f2) holds
|.(((f1 - f2) . x1) - ((f1 - f2) . x2)).| <= p * |.(x1 - x2).|

let x1, x2 be Real; :: thesis: ( x1 in dom (f1 - f2) & x2 in dom (f1 - f2) implies |.(((f1 - f2) . x1) - ((f1 - f2) . x2)).| <= p * |.(x1 - x2).| )
assume that
A13: x1 in dom (f1 - f2) and
A14: x2 in dom (f1 - f2) ; :: thesis: |.(((f1 - f2) . x1) - ((f1 - f2) . x2)).| <= p * |.(x1 - x2).|
|.(((f1 - f2) . x1) - ((f1 - f2) . x2)).| = |.(((f1 . x1) - (f2 . x1)) - ((f1 - f2) . x2)).| by
.= |.(((f1 . x1) - (f2 . x1)) - ((f1 . x2) - (f2 . x2))).| by
.= |.(((f1 . x1) - (f1 . x2)) - ((f2 . x1) - (f2 . x2))).| ;
then A15: |.(((f1 - f2) . x1) - ((f1 - f2) . x2)).| <= |.((f1 . x1) - (f1 . x2)).| + |.((f2 . x1) - (f2 . x2)).| by COMPLEX1:57;
dom (f2 | ((dom f1) /\ (dom f2))) = (dom f2) /\ ((dom f1) /\ (dom f2)) by RELAT_1:61
.= ((dom f2) /\ (dom f2)) /\ (dom f1) by XBOOLE_1:16
.= dom (f1 - f2) by VALUED_1:12 ;
then A16: |.((f2 . x1) - (f2 . x2)).| <= g * |.(x1 - x2).| by ;
dom (f1 | ((dom f1) /\ (dom f2))) = (dom f1) /\ ((dom f1) /\ (dom f2)) by RELAT_1:61
.= ((dom f1) /\ (dom f1)) /\ (dom f2) by XBOOLE_1:16
.= dom (f1 - f2) by VALUED_1:12 ;
then |.((f1 . x1) - (f1 . x2)).| <= s * |.(x1 - x2).| by ;
then |.((f1 . x1) - (f1 . x2)).| + |.((f2 . x1) - (f2 . x2)).| <= (s * |.(x1 - x2).|) + (g * |.(x1 - x2).|) by ;
hence |.(((f1 - f2) . x1) - ((f1 - f2) . x2)).| <= p * |.(x1 - x2).| by ; :: thesis: verum
end;
hence for b1 being PartFunc of REAL,REAL st b1 = f1 - f2 holds
b1 is Lipschitzian ; :: thesis: verum