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 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 A8, A10;
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 A12:
(
x1 in dom (f1 - f2) &
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 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;
verum end;
hence
for b1 being PartFunc of REAL, the carrier of S st b1 = f1 - f2 holds
b1 is Lipschitzian
; verum