theorem asymTT5:
for
a,
b,
p,
q,
r,
s being
Real for
f being
Function of
REAL,
REAL st
a > 0 &
p > 0 & ( for
x being
Real holds
f . x = max (
r,
(min (s,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) ) holds
f is
Lipschitzian