let c be Real; :: thesis: for f, g, F being Function of REAL,REAL st f is Lipschitzian & g is Lipschitzian & f . c = g . c & F = (f | ].-infty,c.[) +* (g | [.c,+infty.[) holds
F is Lipschitzian
let f, g, F be Function of REAL,REAL; :: thesis: ( f is Lipschitzian & g is Lipschitzian & f . c = g . c & F = (f | ].-infty,c.[) +* (g | [.c,+infty.[) implies F is Lipschitzian )
assume that
A1: f is Lipschitzian and
A2: g is Lipschitzian and
A3: f . c = g . c and
A4: F = (f | ].-infty,c.[) +* (g | [.c,+infty.[) ; :: thesis: F is Lipschitzian
cR: c in REAL by XREAL_0:def 1;
then Dfc: c in dom f by FUNCT_2:def 1;
Dgc: c in dom g by FUNCT_2:def 1, cR;
consider rf being Real such that
RF: 0 < rf and
A5: for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= rf * |.(x1 - x2).| by A1;
consider rg being Real such that
0 < rg and
A6: for x1, x2 being Real st x1 in dom g & x2 in dom g holds
|.((g . x1) - (g . x2)).| <= rg * |.(x1 - x2).| by A2;
ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom F & x2 in dom F holds
|.((F . x1) - (F . x2)).| <= r * |.(x1 - x2).| ) )

proof

take max (rf,rg) ; :: thesis: ( 0 < max (rf,rg) & ( for x1, x2 being Real st x1 in dom F & x2 in dom F holds
|.((F . x1) - (F . x2)).| <= (max (rf,rg)) * |.(x1 - x2).| ) )
A7: max (rf,rg) > 0 by RF, XXREAL_0:25;
for x1, x2 being Real st x1 in dom F & x2 in dom F holds
|.((F . x1) - (F . x2)).| <= (max (rf,rg)) * |.(x1 - x2).|

proof

let x1, x2 be Real; :: thesis: ( x1 in dom F & x2 in dom F implies |.((F . x1) - (F . x2)).| <= (max (rf,rg)) * |.(x1 - x2).| )
assume that
x1 in dom F and
x2 in dom F ; :: thesis: |.((F . x1) - (F . x2)).| <= (max (rf,rg)) * |.(x1 - x2).|
( x1 in REAL & x2 in REAL ) by XREAL_0:def 1;
then Dx: ( x1 in dom f & x1 in dom g & x2 in dom f & x2 in dom g ) by FUNCT_2:def 1;

per cases ( x1 < c or x1 >= c ) ;

suppose B1: x1 < c ; :: thesis: |.((F . x1) - (F . x2)).| <= (max (rf,rg)) * |.(x1 - x2).|

then B7: not x1 in dom (g | [.c,+infty.[) by XXREAL_1:236;

per cases ( x2 < c or x2 >= c ) ;

suppose B2: x2 < c ; :: thesis: |.((F . x1) - (F . x2)).| <= (max (rf,rg)) * |.(x1 - x2).|

then B14: not x2 in dom (g | [.c,+infty.[) by XXREAL_1:236;
B15: |.((F . x1) - (F . x2)).| = |.(((f | ].-infty,c.[) . x1) - (((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x2)).| by FUNCT_4:11, B7, A4
.= |.(((f | ].-infty,c.[) . x1) - ((f | ].-infty,c.[) . x2)).| by FUNCT_4:11, B14
.= |.((f . x1) - ((f | ].-infty,c.[) . x2)).| by FUNCT_1:49, XXREAL_1:233, B1 ;
0 <= |.(x1 - x2).| by COMPLEX1:46;
then B17: rf * |.(x1 - x2).| <= (max (rf,rg)) * |.(x1 - x2).| by XREAL_1:64, XXREAL_0:25;
|.((f . x1) - (f . x2)).| <= rf * |.(x1 - x2).| by A5, Dx;
then |.((f . x1) - (f . x2)).| <= (max (rf,rg)) * |.(x1 - x2).| by XXREAL_0:2, B17;
hence |.((F . x1) - (F . x2)).| <= (max (rf,rg)) * |.(x1 - x2).| by B15, FUNCT_1:49, XXREAL_1:233, B2; :: thesis: verum

end;

suppose B3: x2 >= c ; :: thesis: |.((F . x1) - (F . x2)).| <= (max (rf,rg)) * |.(x1 - x2).|

then x2 in [.c,+infty.[ by XXREAL_1:236;
then B6: x2 in dom (g | [.c,+infty.[) by FUNCT_2:def 1;
B9: |.((F . x1) - (F . x2)).| = |.(((f | ].-infty,c.[) . x1) - (((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x2)).| by FUNCT_4:11, B7, A4
.= |.(((f | ].-infty,c.[) . x1) - ((g | [.c,+infty.[) . x2)).| by FUNCT_4:13, B6
.= |.((f . x1) - ((g | [.c,+infty.[) . x2)).| by FUNCT_1:49, XXREAL_1:233, B1 ;
B8: ( |.((f . x1) - (f . c)).| <= rf * |.(x1 - c).| & |.((g . c) - (g . x2)).| <= rg * |.(c - x2).| ) by A5, A6, Dx, Dfc, Dgc;
( |.(x1 - c).| >= 0 & |.(c - x2).| >= 0 ) by COMPLEX1:46;
then ( rf * |.(x1 - c).| <= (max (rf,rg)) * |.(x1 - c).| & rg * |.(c - x2).| <= (max (rf,rg)) * |.(c - x2).| ) by XREAL_1:64, XXREAL_0:25;
then ( |.((f . x1) - (f . c)).| <= (max (rf,rg)) * |.(x1 - c).| & |.((g . c) - (g . x2)).| <= (max (rf,rg)) * |.(c - x2).| ) by XXREAL_0:2, B8;
then ( |.((f . x1) - (f . c)).| <= (max (rf,rg)) * (- (x1 - c)) & |.((g . c) - (g . x2)).| <= (max (rf,rg)) * (- (c - x2)) ) by COMPLEX1:70, B3, XREAL_1:47, B1;
then B12X: |.((f . x1) - (f . c)).| + |.((g . c) - (g . x2)).| <= ((max (rf,rg)) * (- (x1 - c))) + ((max (rf,rg)) * (- (c - x2))) by XREAL_1:7;
B13: |.((f . x1) - (g . x2)).| <= |.((f . x1) - (f . c)).| + |.((f . c) - (g . x2)).| by COMPLEX1:63;
x2 - x1 <= |.(x2 - x1).| by COMPLEX1:76;
then x2 - x1 <= |.(x1 - x2).| by COMPLEX1:60;
then (x2 - x1) * (max (rf,rg)) <= |.(x1 - x2).| * (max (rf,rg)) by A7, XREAL_1:64;
then |.((f . x1) - (f . c)).| + |.((g . c) - (g . x2)).| <= (max (rf,rg)) * |.(x1 - x2).| by XXREAL_0:2, B12X;
then |.((f . x1) - (g . x2)).| <= (max (rf,rg)) * |.(x1 - x2).| by XXREAL_0:2, B13, A3;
hence |.((F . x1) - (F . x2)).| <= (max (rf,rg)) * |.(x1 - x2).| by B9, FUNCT_1:49, XXREAL_1:236, B3; :: thesis: verum

end;

end;

end;

suppose C1: x1 >= c ; :: thesis: |.((F . x1) - (F . x2)).| <= (max (rf,rg)) * |.(x1 - x2).|

then x1 in [.c,+infty.[ by XXREAL_1:236;
then C5: x1 in dom (g | [.c,+infty.[) by FUNCT_2:def 1;

per cases ( x2 < c or x2 >= c ) ;

suppose C2: x2 < c ; :: thesis: |.((F . x1) - (F . x2)).| <= (max (rf,rg)) * |.(x1 - x2).|

then C6: not x2 in dom (g | [.c,+infty.[) by XXREAL_1:236;
C12: |.((F . x1) - (F . x2)).| = |.(((g | [.c,+infty.[) . x1) - (((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x2)).| by FUNCT_4:13, C5, A4
.= |.(((g | [.c,+infty.[) . x1) - ((f | ].-infty,c.[) . x2)).| by FUNCT_4:11, C6
.= |.((g . x1) - ((f | ].-infty,c.[) . x2)).| by FUNCT_1:49, XXREAL_1:236, C1 ;
C9: ( |.((g . x1) - (g . c)).| <= rg * |.(x1 - c).| & |.((f . c) - (f . x2)).| <= rf * |.(c - x2).| ) by A5, A6, Dx, Dfc, Dgc;
( |.(x1 - c).| >= 0 & |.(c - x2).| >= 0 ) by COMPLEX1:46;
then ( rg * |.(x1 - c).| <= (max (rf,rg)) * |.(x1 - c).| & rf * |.(c - x2).| <= (max (rf,rg)) * |.(c - x2).| ) by XREAL_1:64, XXREAL_0:25;
then ( |.((g . x1) - (g . c)).| <= (max (rf,rg)) * |.(x1 - c).| & |.((f . c) - (f . x2)).| <= (max (rf,rg)) * |.(c - x2).| ) by XXREAL_0:2, C9;
then ( |.((g . x1) - (g . c)).| <= (max (rf,rg)) * (x1 - c) & |.((f . c) - (f . x2)).| <= (max (rf,rg)) * (c - x2) ) by COMPLEX1:43, C2, C1, XREAL_1:48;
then C10: |.((g . x1) - (g . c)).| + |.((f . c) - (f . x2)).| <= ((max (rf,rg)) * (x1 - c)) + ((max (rf,rg)) * (c - x2)) by XREAL_1:7;
C11: |.((g . x1) - (f . x2)).| <= |.((g . x1) - (g . c)).| + |.((g . c) - (f . x2)).| by COMPLEX1:63;
(x1 - x2) * (max (rf,rg)) <= |.(x1 - x2).| * (max (rf,rg)) by A7, XREAL_1:64, COMPLEX1:76;
then |.((g . x1) - (g . c)).| + |.((f . c) - (f . x2)).| <= (max (rf,rg)) * |.(x1 - x2).| by XXREAL_0:2, C10;
then |.((g . x1) - (f . x2)).| <= (max (rf,rg)) * |.(x1 - x2).| by XXREAL_0:2, C11, A3;
hence |.((F . x1) - (F . x2)).| <= (max (rf,rg)) * |.(x1 - x2).| by FUNCT_1:49, XXREAL_1:233, C2, C12; :: thesis: verum

end;

suppose C3: x2 >= c ; :: thesis: |.((F . x1) - (F . x2)).| <= (max (rf,rg)) * |.(x1 - x2).|

then x2 in [.c,+infty.[ by XXREAL_1:236;
then C8: x2 in dom (g | [.c,+infty.[) by FUNCT_2:def 1;
C13: |.((F . x1) - (F . x2)).| = |.(((g | [.c,+infty.[) . x1) - (((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x2)).| by FUNCT_4:13, C5, A4
.= |.(((g | [.c,+infty.[) . x1) - ((g | [.c,+infty.[) . x2)).| by FUNCT_4:13, C8
.= |.((g . x1) - ((g | [.c,+infty.[) . x2)).| by FUNCT_1:49, XXREAL_1:236, C1 ;
0 <= |.(x1 - x2).| by COMPLEX1:46;
then C14: rg * |.(x1 - x2).| <= (max (rf,rg)) * |.(x1 - x2).| by XREAL_1:64, XXREAL_0:25;
|.((g . x1) - (g . x2)).| <= rg * |.(x1 - x2).| by A6, Dx;
then |.((g . x1) - (g . x2)).| <= (max (rf,rg)) * |.(x1 - x2).| by XXREAL_0:2, C14;
hence |.((F . x1) - (F . x2)).| <= (max (rf,rg)) * |.(x1 - x2).| by C13, FUNCT_1:49, XXREAL_1:236, C3; :: thesis: verum

end;

end;

end;

end;

end;

hence ( 0 < max (rf,rg) & ( for x1, x2 being Real st x1 in dom F & x2 in dom F holds
|.((F . x1) - (F . x2)).| <= (max (rf,rg)) * |.(x1 - x2).| ) ) by RF, XXREAL_0:25; :: thesis: verum

end;

hence F is Lipschitzian ; :: thesis: verum