set X = dom f1;
set X1 = dom f2;
consider s being Real such that
A1:
0 < s
and
A2:
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
A3:
0 < g
and
A4:
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 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;
( 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 A1, A3;
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;
( x1 in dom (f1 + f2) & x2 in dom (f1 + f2) implies |.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| <= p * |.(x1 - x2).| )assume that A5:
x1 in dom (f1 + f2)
and A6:
x2 in dom (f1 + f2)
;
|.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| <= p * |.(x1 - x2).||.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| =
|.(((f1 . x1) + (f2 . x1)) - ((f1 + f2) . x2)).|
by A5, VALUED_1:def 1
.=
|.(((f1 . x1) + (f2 . x1)) - ((f1 . x2) + (f2 . x2))).|
by A6, VALUED_1:def 1
.=
|.(((f1 . x1) - (f1 . x2)) + ((f2 . x1) - (f2 . x2))).|
;
then A7:
|.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| <= |.((f1 . x1) - (f1 . x2)).| + |.((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:
|.((f2 . x1) - (f2 . x2)).| <= g * |.(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
|.((f1 . x1) - (f1 . x2)).| <= s * |.(x1 - x2).|
by A2, A5, A6;
then
|.((f1 . x1) - (f1 . x2)).| + |.((f2 . x1) - (f2 . x2)).| <= (s * |.(x1 - x2).|) + (g * |.(x1 - x2).|)
by A8, XREAL_1:7;
hence
|.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| <= p * |.(x1 - x2).|
by A7, XXREAL_0:2;
verum end;
hence
for b1 being PartFunc of REAL,REAL st b1 = f1 + f2 holds
b1 is Lipschitzian
; verum