let a, b, c, r be Real; :: thesis: for f being Function of REAL,REAL st a < b & b < c & r <> 0 & ( for x being Real holds f . x = (r (#) (TriangularFS (a,b,c))) . x ) holds
centroid (f,['a,c']) = ((a + b) + c) / 3
let f be Function of REAL,REAL; :: thesis: ( a < b & b < c & r <> 0 & ( for x being Real holds f . x = (r (#) (TriangularFS (a,b,c))) . x ) implies centroid (f,['a,c']) = ((a + b) + c) / 3 )
assume that
A1: ( a < b & b < c ) and
A2: r <> 0 and
A3: for x being Real holds f . x = (r (#) (TriangularFS (a,b,c))) . x ; :: thesis: centroid (f,['a,c']) = ((a + b) + c) / 3
A4: f | [.a,c.] = ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) | [.a,b.]) +* ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) | [.b,c.]) by Th7, A1, A3;
set F = r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))));
set G = r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))));
A6: ( b - a > 0 & c - b > 0 ) by XREAL_1:50, A1;
A9: c - a <> 0 by A1;
( (r * (b - a)) / 2 <> 0 & (r * (c - b)) / 2 <> 0 )

proof

per cases ( r > 0 or r < 0 ) by A2;

suppose r > 0 ; :: thesis: ( (r * (b - a)) / 2 <> 0 & (r * (c - b)) / 2 <> 0 )

hence ( (r * (b - a)) / 2 <> 0 & (r * (c - b)) / 2 <> 0 ) by A6; :: thesis: verum

end;

suppose r < 0 ; :: thesis: ( (r * (b - a)) / 2 <> 0 & (r * (c - b)) / 2 <> 0 )

hence ( (r * (b - a)) / 2 <> 0 & (r * (c - b)) / 2 <> 0 ) by A6; :: thesis: verum

end;

end;

end;

then ( integral ((r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))),['a,b']) <> 0 & integral ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))),['b,c']) <> 0 & (r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a)))))) . b = (r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))) . b ) by Th901, A1, Th902, Th903;
hence centroid (f,['a,c']) = (1 / (integral (f,['a,c']))) * ((integral (((id REAL) (#) (r (#) (AffineMap ((1 / (b - a)),(- (a / (b - a))))))),['a,b'])) + (integral (((id REAL) (#) (r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b)))))),['b,c']))) by FUZZY817, A4, A1
.= (1 / (integral (f,['a,c']))) * ((integral (((id REAL) (#) (AffineMap ((r * (1 / (b - a))),(r * (- (a / (b - a))))))),['a,b'])) + (integral (((id REAL) (#) (r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b)))))),['b,c']))) by FUZZY_7:13
.= (1 / (integral (f,['a,c']))) * ((integral (((id REAL) (#) (AffineMap ((r * (1 / (b - a))),(r * (- (a / (b - a))))))),['a,b'])) + (integral (((id REAL) (#) (AffineMap ((r * (- (1 / (c - b)))),(r * (c / (c - b)))))),['b,c']))) by FUZZY_7:13
.= (1 / (integral (f,['a,c']))) * (((b - a) * ((((r * (1 / (b - a))) * (((b * b) + (b * a)) + (a * a))) / 3) + (((r * (- (a / (b - a)))) * (b + a)) / 2))) + (integral (((id REAL) (#) (AffineMap ((r * (- (1 / (c - b)))),(r * (c / (c - b)))))),['b,c']))) by FUZZY_8:42, A1
.= (1 / (integral (f,['a,c']))) * (((b - a) * ((((r * (1 / (b - a))) * (((b * b) + (b * a)) + (a * a))) / 3) + (((r * (- (a / (b - a)))) * (b + a)) / 2))) + ((c - b) * ((((r * (- (1 / (c - b)))) * (((c * c) + (c * b)) + (b * b))) / 3) + (((r * (c / (c - b))) * (c + b)) / 2)))) by FUZZY_8:42, A1
.= (1 / ((r * (c - a)) / 2)) * (((((((b - a) * (r * (1 / (b - a)))) * (((b * b) + (b * a)) + (a * a))) / 3) + ((((b - a) * (r * (- (a / (b - a))))) * (b + a)) / 2)) + ((((c - b) * (r * (- (1 / (c - b))))) * (((c * c) + (c * b)) + (b * b))) / 3)) + ((((c - b) * (r * (c / (c - b)))) * (c + b)) / 2)) by Th6, A1, A3
.= (1 / ((r * (c - a)) / 2)) * (((((((b - a) * ((r * 1) / (b - a))) * (((b * b) + (b * a)) + (a * a))) / 3) + ((((b - a) * (r * (- (a / (b - a))))) * (b + a)) / 2)) + ((((c - b) * (r * (- (1 / (c - b))))) * (((c * c) + (c * b)) + (b * b))) / 3)) + ((((c - b) * (r * (c / (c - b)))) * (c + b)) / 2)) by XCMPLX_1:74
.= (1 / ((r * (c - a)) / 2)) * (((((((b - a) * (r / (b - a))) * (((b * b) + (b * a)) + (a * a))) / 3) - ((((b - a) * (r * (a / (b - a)))) * (b + a)) / 2)) - ((((c - b) * (r * (1 / (c - b)))) * (((c * c) + (c * b)) + (b * b))) / 3)) + ((((c - b) * ((r * c) / (c - b))) * (c + b)) / 2)) by XCMPLX_1:74
.= (1 / ((r * (c - a)) / 2)) * (((((((b - a) * (r / (b - a))) * (((b * b) + (b * a)) + (a * a))) / 3) - ((((b - a) * ((r * a) / (b - a))) * (b + a)) / 2)) - ((((c - b) * (r * (1 / (c - b)))) * (((c * c) + (c * b)) + (b * b))) / 3)) + ((((c - b) * ((r * c) / (c - b))) * (c + b)) / 2)) by XCMPLX_1:74
.= (1 / ((r * (c - a)) / 2)) * (((((((b - a) * (r / (b - a))) * (((b * b) + (b * a)) + (a * a))) / 3) - ((((b - a) * ((r * a) / (b - a))) * (b + a)) / 2)) - ((((c - b) * ((r * 1) / (c - b))) * (((c * c) + (c * b)) + (b * b))) / 3)) + ((((c - b) * ((r * c) / (c - b))) * (c + b)) / 2)) by XCMPLX_1:74
.= (1 / ((r * (c - a)) / 2)) * (((((r * (((b * b) + (b * a)) + (a * a))) / 3) - ((((b - a) * ((r * a) / (b - a))) * (b + a)) / 2)) - ((((c - b) * (r / (c - b))) * (((c * c) + (c * b)) + (b * b))) / 3)) + ((((c - b) * ((r * c) / (c - b))) * (c + b)) / 2)) by XCMPLX_1:87, A6
.= (1 / ((r * (c - a)) / 2)) * (((((r * (((b * b) + (b * a)) + (a * a))) / 3) - (((r * a) * (b + a)) / 2)) - ((((c - b) * (r / (c - b))) * (((c * c) + (c * b)) + (b * b))) / 3)) + ((((c - b) * ((r * c) / (c - b))) * (c + b)) / 2)) by XCMPLX_1:87, A6
.= (1 / ((r * (c - a)) / 2)) * (((((r * (((b * b) + (b * a)) + (a * a))) / 3) - (((r * a) * (b + a)) / 2)) - ((r * (((c * c) + (c * b)) + (b * b))) / 3)) + ((((c - b) * ((r * c) / (c - b))) * (c + b)) / 2)) by XCMPLX_1:87, A6
.= (1 / ((r * (c - a)) / 2)) * (((((r * (((b * b) + (b * a)) + (a * a))) / 3) - (((r * a) * (b + a)) / 2)) - ((r * (((c * c) + (c * b)) + (b * b))) / 3)) + (((r * c) * (c + b)) / 2)) by XCMPLX_1:87, A6
.= ((1 * 2) / (r * (c - a))) * (((((r * (((b * b) + (b * a)) + (a * a))) / 3) - (((r * a) * (b + a)) / 2)) - ((r * (((c * c) + (c * b)) + (b * b))) / 3)) + (((r * c) * (c + b)) / 2)) by XCMPLX_1:77
.= ((2 / (r * (c - a))) * r) * (((((((b * b) + (b * a)) + (a * a)) / 3) - ((a * (b + a)) / 2)) - ((((c * c) + (c * b)) + (b * b)) / 3)) + ((c * (c + b)) / 2))
.= ((r / (r * (c - a))) * 2) * (((((((b * b) + (b * a)) + (a * a)) / 3) - ((a * (b + a)) / 2)) - ((((c * c) + (c * b)) + (b * b)) / 3)) + ((c * (c + b)) / 2)) by XCMPLX_1:75
.= (((r / r) / (c - a)) * 2) * (((((((b * b) + (b * a)) + (a * a)) / 3) - ((a * (b + a)) / 2)) - ((((c * c) + (c * b)) + (b * b)) / 3)) + ((c * (c + b)) / 2)) by XCMPLX_1:78
.= ((1 / (c - a)) * 2) * (((((((b * b) + (b * a)) + (a * a)) / 3) - ((a * (b + a)) / 2)) - ((((c * c) + (c * b)) + (b * b)) / 3)) + ((c * (c + b)) / 2)) by XCMPLX_1:60, A2
.= ((1 / (c - a)) * (c - a)) * (((b / 3) + (a / 3)) + (c / 3))
.= ((1 * (c - a)) / (c - a)) * (((b / 3) + (a / 3)) + (c / 3)) by XCMPLX_1:74
.= 1 * (((b / 3) + (a / 3)) + (c / 3)) by XCMPLX_1:60, A9
.= ((a + b) + c) / 3 ;
:: thesis: verum