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

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

suppose B1: b = 0 ; :: 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 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).| ) )
thus 0 < 1 ; :: thesis: for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|
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)).| = |.((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
.= 0 by COMPLEX1:44, B1 ;
hence ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) by COMPLEX1:46; :: thesis: verum

end;

hence f is Lipschitzian ; :: thesis: verum

end;

suppose b <> 0 ; :: thesis: f is Lipschitzian

hence f is Lipschitzian by A1, A2, L724p; :: thesis: verum

end;

end;