theorem
for
a,
b,
c,
d being
Real for
f being
Function of
REAL,
REAL st
b > 0 &
c > 0 &
d > 0 &
d < b & ( for
x being
Real holds
f . x = min (
d,
(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
f | [.(a - c),(a + c).] = (((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(a - c),(a + ((d - b) / (b / c))).]) +* ((AffineMap (0,d)) | [.(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))).])) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(a + ((b - d) / (b / c))),(a + c).])