let a1, c, a2, d be Real; :: thesis:
assume A1: ( c > 0 & d > 0 & a1 < a2 ) ; :: thesis:
set f = d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)));
DAa: a2 - a1 > a1 - a1 by XREAL_1:14, A1;
( a1 - c <= a2 - 0 & a2 + 0 <= a2 + c ) by A1, XREAL_1:13, XREAL_1:7;
then A2: (d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))) | [.(a1 - c),(a2 + c).] = (d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))) | ['(a1 - c),(a2 + c)'] by INTEGRA5:def 3, XXREAL_0:2
.= (((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(a1 - c),a1.]) +* ((AffineMap (0,d)) | [.a1,a2.])) +* ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]) by SymTrape, A1 ;
thus centroid ((d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))),['(a1 - c),(a2 + c)']) = (integral (((id REAL) (#) (d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c))))),['(a1 - c),(a2 + c)'])) / (integral ((d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))),['(a1 - c),(a2 + c)'])) by FUZZY_6:def 1
.= (((integral (((id REAL) (#) (AffineMap ((d / c),(- ((d / c) * (a1 - c)))))),['(a1 - c),a1'])) + (integral (((id REAL) (#) (AffineMap (0,d))),['a1,a2']))) + (integral (((id REAL) (#) (AffineMap ((- (d / c)),((d / c) * (a2 + c))))),['a2,(a2 + c)']))) / (integral ((d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))),['(a1 - c),(a2 + c)'])) by Lm29n, A1, A2
.= ((((1 / 2) * d) * ((c + a2) - a1)) * (a1 + a2)) / (integral ((d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)))),['(a1 - c),(a2 + c)'])) by Lm29n1, A1
.= ((((1 / 2) * d) * ((c + a2) - a1)) * (a1 + a2)) / (((integral ((AffineMap ((d / c),(- ((d / c) * (a1 - c))))),['(a1 - c),a1'])) + (integral ((AffineMap (0,d)),['a1,a2']))) + (integral ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))),['a2,(a2 + c)']))) by Lm29d, A1, A2
.= (((1 / 2) * (a1 + a2)) * (d * ((c + a2) - a1))) / (d * ((a2 - a1) + c)) by Lm29d1, A1
.= (a1 + a2) / 2 by XCMPLX_1:89, DAa, A1 ; :: thesis: