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

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

proof

let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= (|.b.| * |.(1 / c).|) * |.(x1 - x2).| )
T1: |.((f . x1) - (f . x2)).| = |.((min (d,(max (e,(b - |.((b * (x1 - a)) / c).|))))) - (f . x2)).| by A1
.= |.((min (d,(max (e,(b - |.((b * (x1 - a)) / c).|))))) - (min (d,(max (e,(b - |.((b * (x2 - a)) / c).|)))))).| by A1 ;
T2: |.((f . x1) - (f . x2)).| <= |.((b - |.((b * (x1 - a)) / c).|) - (b - |.((b * (x2 - a)) / c).|)).| by T1, F51;
T41: |.(|.((b * (x2 - a)) / c).| - |.((b * (x1 - a)) / c).|).| <= |.(((b * (x2 - a)) / c) - ((b * (x1 - a)) / c)).| by COMPLEX1:64;
|.(((b * (x2 - a)) / c) - ((b * (x1 - a)) / c)).| = |.((b * ((x2 - a) / c)) - ((b * (x1 - a)) / c)).| by XCMPLX_1:74
.= |.((b * ((x2 - a) / c)) - (b * ((x1 - a) / c))).| by XCMPLX_1:74
.= |.(b * (((x2 - a) / c) - ((x1 - a) / c))).|
.= |.b.| * |.(((x2 - a) / c) - ((x1 - a) / c)).| by COMPLEX1:65
.= |.b.| * |.(((x2 - a) * (1 / c)) - ((x1 - a) / c)).| by XCMPLX_1:99
.= |.b.| * |.(((x2 - a) * (1 / c)) - ((x1 - a) * (1 / c))).| by XCMPLX_1:99
.= |.b.| * |.((1 / c) * ((x2 - a) - (x1 - a))).|
.= |.b.| * (|.(1 / c).| * |.((x2 - a) - (x1 - a)).|) by COMPLEX1:65
.= (|.b.| * |.(1 / c).|) * |.(x2 - x1).|
.= (|.b.| * |.(1 / c).|) * |.(x1 - x2).| by COMPLEX1:60 ;
hence ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= (|.b.| * |.(1 / c).|) * |.(x1 - x2).| ) by T41, T2, XXREAL_0:2; :: thesis: verum

end;

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

end;

hence f is Lipschitzian ; :: thesis: verum