theorem :: FUZZY_9:24

for p, q, s, t being Real
for f, F being Function of REAL,REAL st p * s < 0 & p > 0 & ((p * t) - (q * s)) / (p - s) > 0 & f = ((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[) & F = max+ f holds
centroid (F,['(- (q / p)),(- (t / s))']) = (((- (q / p)) + ((t - q) / (p - s))) + (- (t / s))) / 3