set X = dom f1;
set X1 = dom f2;
consider s being real number such that
A1: 0 < s and
A2: for x1, x2 being real number st x1 in dom (f1 | ((dom f1) /\ (dom f2))) & x2 in dom (f1 | ((dom f1) /\ (dom f2))) holds
abs ((f1 . x1) - (f1 . x2)) <= s * (abs (x1 - x2)) by Th33;
consider g being real number such that
A3: 0 < g and
A4: for x1, x2 being real number st x1 in dom (f2 | ((dom f1) /\ (dom f2))) & x2 in dom (f2 | ((dom f1) /\ (dom f2))) holds
abs ((f2 . x1) - (f2 . x2)) <= g * (abs (x1 - x2)) by Th33;

now

take p = s + g; :: thesis: ( 0 < p & ( for x1, x2 being real number st x1 in dom (f1 + f2) & x2 in dom (f1 + f2) holds
abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) <= p * (abs (x1 - x2)) ) )
thus 0 < p by A1, A3; :: thesis: for x1, x2 being real number st x1 in dom (f1 + f2) & x2 in dom (f1 + f2) holds
abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) <= p * (abs (x1 - x2))
let x1, x2 be real number ; :: thesis: ( x1 in dom (f1 + f2) & x2 in dom (f1 + f2) implies abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) <= p * (abs (x1 - x2)) )
assume that
A5: x1 in dom (f1 + f2) and
A6: x2 in dom (f1 + f2) ; :: thesis: abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) <= p * (abs (x1 - x2))
abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) = abs (((f1 . x1) + (f2 . x1)) - ((f1 + f2) . x2)) by A5, VALUED_1:def 1
.= abs (((f1 . x1) + (f2 . x1)) - ((f1 . x2) + (f2 . x2))) by A6, VALUED_1:def 1
.= abs (((f1 . x1) - (f1 . x2)) + ((f2 . x1) - (f2 . x2))) ;
then A7: abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) <= (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) by COMPLEX1:56;
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:def 1 ;
then A8: abs ((f2 . x1) - (f2 . x2)) <= g * (abs (x1 - x2)) by A4, A5, A6;
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:def 1 ;
then abs ((f1 . x1) - (f1 . x2)) <= s * (abs (x1 - x2)) by A2, A5, A6;
then (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) <= (s * (abs (x1 - x2))) + (g * (abs (x1 - x2))) by A8, XREAL_1:7;
hence abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) <= p * (abs (x1 - x2)) by A7, 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