theorem :: FUZZY_8:34

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