let p, q, s, t be Real; :: thesis: 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
let f, F be Function of REAL,REAL; :: thesis: ( 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 implies centroid (F,['(- (q / p)),(- (t / s))']) = (((- (q / p)) + ((t - q) / (p - s))) + (- (t / s))) / 3 )
assume that
A1: ( p * s < 0 & p > 0 ) and
A0: ((p * t) - (q * s)) / (p - s) > 0 and
A2: f = ((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[) and
A5: F = max+ f ; :: thesis: centroid (F,['(- (q / p)),(- (t / s))']) = (((- (q / p)) + ((t - q) / (p - s))) + (- (t / s))) / 3
A3: ( - (q / p) < (t - q) / (p - s) & (t - q) / (p - s) < - (t / s) ) by Th13, A1, A0;
for x being Real holds F . x = ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x

proof

let x be Real; :: thesis: F . x = ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x
set ff = ((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[);
reconsider ff = ((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[) as Function of REAL,REAL by FUZZY_7:12;
for x being Real holds ff . x = (((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x ;
hence F . x = ((((p * t) - (q * s)) / (p - s)) (#) (TriangularFS ((- (q / p)),((t - q) / (p - s)),(- (t / s))))) . x by Th26, A1, A0, A2, A5; :: thesis: verum

end;

hence centroid (F,['(- (q / p)),(- (t / s))']) = (((- (q / p)) + ((t - q) / (p - s))) + (- (t / s))) / 3 by Th25, A3, A0; :: thesis: verum