let f be Function of REAL,REAL; :: thesis: for a, b, c, r, s being Real st b <> 0 & ( for x being Real holds f . x = max (r,(min (s,(c * (1 - |.((x - a) / b).|))))) ) holds
f is Lipschitzian
let a, b, c, r, s be Real; :: thesis: ( b <> 0 & ( for x being Real holds f . x = max (r,(min (s,(c * (1 - |.((x - a) / b).|))))) ) implies f is Lipschitzian )
assume A3: b <> 0 ; :: thesis: ( ex x being Real st not f . x = max (r,(min (s,(c * (1 - |.((x - a) / b).|))))) or f is Lipschitzian )
assume A1: for x being Real holds f . x = max (r,(min (s,(c * (1 - |.((x - a) / b).|))))) ; :: thesis: f is Lipschitzian
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

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

suppose C0: c = 0 ; :: thesis: 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).| ) )

take 1 ; :: thesis: ( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) )
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|

proof

let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| )
|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,(c * (1 - |.((x1 - a) / b).|)))))) - (f . x2)).| by A1
.= |.((max (r,(min (s,(0 * (1 - |.((x1 - a) / b).|)))))) - (max (r,(min (s,(0 * (1 - |.((x2 - a) / b).|))))))).| by C0, A1
.= 0 by COMPLEX1:44 ;
hence ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) by COMPLEX1:46; :: thesis: verum

end;

hence ( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) ) ; :: thesis: verum

end;

suppose A2: c <> 0 ; :: thesis: 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).| ) )

take (1 / |.b.|) * |.c.| ; :: thesis: ( 0 < (1 / |.b.|) * |.c.| & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= ((1 / |.b.|) * |.c.|) * |.(x1 - x2).| ) )
A5: ( |.c.| > 0 & |.b.| > 0 ) by A2, A3, COMPLEX1:47;
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= ((1 / |.b.|) * |.c.|) * |.(x1 - x2).|

proof

let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= ((1 / |.b.|) * |.c.|) * |.(x1 - x2).| )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= ((1 / |.b.|) * |.c.|) * |.(x1 - x2).|
|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,(c * (1 - |.((x1 - a) / b).|)))))) - (f . x2)).| by A1
.= |.((max (r,(min (s,(c * (1 - |.((x1 - a) / b).|)))))) - (max (r,(min (s,(c * (1 - |.((x2 - a) / b).|))))))).| by A1 ;
then A9: |.((f . x1) - (f . x2)).| <= |.((c * (1 - |.((x1 - a) / b).|)) - (c * (1 - |.((x2 - a) / b).|))).| by LeMM01;
|.(((x1 - a) / b) - ((x2 - a) / b)).| = |.(((x1 - a) - (x2 - a)) / b).| by XCMPLX_1:120
.= |.(x1 - x2).| / |.b.| by COMPLEX1:67 ;
then |.(|.((x1 - a) / b).| - |.((x2 - a) / b).|).| * |.c.| <= (|.(x1 - x2).| / |.b.|) * |.c.| by XREAL_1:64, A5, COMPLEX1:64;
then |.c.| * |.(|.((x2 - a) / b).| - |.((x1 - a) / b).|).| <= (|.(x1 - x2).| / |.b.|) * |.c.| by COMPLEX1:60;
then |.(c * ((- |.((x1 - a) / b).|) + |.((x2 - a) / b).|)).| <= (|.(x1 - x2).| / |.b.|) * |.c.| by COMPLEX1:65;
then |.((c * (1 - |.((x1 - a) / b).|)) - (c * (1 - |.((x2 - a) / b).|))).| <= ((1 / |.b.|) * |.c.|) * |.(x1 - x2).| by XCMPLX_1:101;
hence |.((f . x1) - (f . x2)).| <= ((1 / |.b.|) * |.c.|) * |.(x1 - x2).| by XXREAL_0:2, A9; :: thesis: verum

end;

hence ( 0 < (1 / |.b.|) * |.c.| & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= ((1 / |.b.|) * |.c.|) * |.(x1 - x2).| ) ) by A5; :: thesis: verum

end;

end;

end;

hence f is Lipschitzian ; :: thesis: verum