let a, b, c, d be Real; :: thesis: ( a < b & b < c & b - a = c - b & d <> 0 implies centroid ((d (#) (TriangularFS (a,b,c))),['a,c']) = b )
assume that
A1: ( a < b & b < c ) and
A2: b - a = c - b and
D1: d <> 0 ; :: thesis: centroid ((d (#) (TriangularFS (a,b,c))),['a,c']) = b
( TriangularFS (a,b,c) is_integrable_on ['a,c'] & (TriangularFS (a,b,c)) | ['a,c'] is bounded ) by Lm21L, A1;
then centroid ((d (#) (TriangularFS (a,b,c))),['a,c']) = centroid ((TriangularFS (a,b,c)),['a,c']) by FUZZY_6:32, D1;
hence centroid ((d (#) (TriangularFS (a,b,c))),['a,c']) = b by Lm21, A1, A2; :: thesis: verum