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

proof

let x be Real; :: thesis: f . x = max (0,(min (b,(b * (1 - |.((x - a) / c).|)))))
max (0,(min (b,(b * (1 - |.((x - a) / c).|))))) = max (0,(min (b,((b * 1) - (b * |.((x - a) / c).|)))))
.= max (0,(min (b,(b - (|.b.| * |.((x - a) / c).|))))) by A1, ABSVALUE:def 1
.= max (0,(min (b,(b - |.(b * ((x - a) / c)).|)))) by COMPLEX1:65
.= max (0,(min (b,(b - |.((b * (x - a)) / c).|)))) by XCMPLX_1:74
.= max (0,(b - |.((b * (x - a)) / c).|)) by XXREAL_0:def 9, Lm5 ;
hence f . x = max (0,(min (b,(b * (1 - |.((x - a) / c).|))))) by A3; :: thesis: verum

end;

hence f is Lipschitzian by FUZZY_5:70, A2; :: thesis: verum