set X = dom f1;
set X1 = dom f2;
consider s being Real such that
A8: 0 < s and
A9: 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 Th26;
consider g being Real such that
A10: 0 < g and
A11: 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 Th26;

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 A8, A10; :: 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 A12: ( x1 in dom (f1 - f2) & 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 A12, VFUNCT_1:def 2
.= ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 /. x2) - (f2 /. x2))).|| by A12, VFUNCT_1:def 2
.= ||.((f1 /. x1) - ((f2 /. x1) + ((f1 /. x2) - (f2 /. x2)))).|| by RLVECT_1:27
.= ||.((f1 /. x1) - (((f1 /. x2) + (f2 /. x1)) - (f2 /. x2))).|| by RLVECT_1:28
.= ||.((f1 /. x1) - ((f1 /. x2) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:28
.= ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:27 ;
then A13: ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by NORMSP_1:3;
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 VFUNCT_1:def 2 ;
then A14: ||.((f2 /. x1) - (f2 /. x2)).|| <= g * |.(x1 - x2).| by A11, A12;
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 VFUNCT_1:def 2 ;
then ||.((f1 /. x1) - (f1 /. x2)).|| <= s * |.(x1 - x2).| by A9, A12;
then ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| <= (s * |.(x1 - x2).|) + (g * |.(x1 - x2).|) by A14, XREAL_1:7;
hence ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * |.(x1 - x2).| by A13, XXREAL_0:2; :: thesis: verum

end;

hence for b₁ being PartFunc of REAL, the carrier of S st b₁ = f1 - f2 holds
b₁ is Lipschitzian ; :: thesis: verum