theorem :: FUZZY_8:43

for a, b, c, d, r, s being Real
for f being Function of REAL,REAL st a < b & b < c & c < d & f | [.a,d.] = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,d.]) holds
centroid (f,['a,d']) = ((((b - a) * ((((r / (b - a)) * (((b * b) + (b * a)) + (a * a))) / 3) + (((- ((a * r) / (b - a))) * (b + a)) / 2))) + ((c - b) * (((((s - r) / (c - b)) * (((c * c) + (c * b)) + (b * b))) / 3) + (((s - ((c * (s - r)) / (c - b))) * (c + b)) / 2)))) + ((d - c) * (((((- s) / (d - c)) * (((d * d) + (d * c)) + (c * c))) / 3) + (((- ((d * (- s)) / (d - c))) * (d + c)) / 2)))) / ((((b - a) * ((((r / (b - a)) * (b + a)) / 2) + (- ((a * r) / (b - a))))) + ((c - b) * (((((s - r) / (c - b)) * (c + b)) / 2) + (s - ((c * (s - r)) / (c - b)))))) + ((d - c) * (((((- s) / (d - c)) * (d + c)) / 2) + (- ((d * (- s)) / (d - c))))))