let a, b, c, d be Real; :: thesis: 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
centroid (f,['(a - c),(a + c)']) = a
let f be Function of REAL,REAL; :: thesis: ( b > 0 & c > 0 & d > 0 & d < b & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) implies centroid (f,['(a - c),(a + c)']) = a )
assume A1: ( b > 0 & c > 0 & d > 0 & d < b ) ; :: thesis: ( ex x being Real st not f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) or centroid (f,['(a - c),(a + c)']) = a )
assume for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ; :: thesis: centroid (f,['(a - c),(a + c)']) = a
hence centroid (f,['(a - c),(a + c)']) = centroid ((d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))),['(a - c),(a + c)']) by Lm220, A1
.= a by Lm223, A1 ;
:: thesis: verum