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