theorem :: FUZZY_6:48

for A being non empty closed_interval Subset of REAL
for a, b, p, q, c, d, e being Real
for f being Function of REAL,REAL st a <> p & f | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) & (q - b) / (a - p) in A holds
centroid (f,A) = ((((((1 / 3) * a) * ((((q - b) / (a - p)) ^3) - ((lower_bound A) ^3))) + (((1 / 2) * b) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2)))) + (((1 / 3) * p) * (((upper_bound A) ^3) - (((q - b) / (a - p)) ^3)))) + (((1 / 2) * q) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2)))) / ((((((1 / 2) * a) * ((((q - b) / (a - p)) ^2) - ((lower_bound A) ^2))) + (b * (((q - b) / (a - p)) - (lower_bound A)))) + (((1 / 2) * p) * (((upper_bound A) ^2) - (((q - b) / (a - p)) ^2)))) + (q * ((upper_bound A) - ((q - b) / (a - p)))))