let a1, c, a2, d be Real; :: thesis: ( c > 0 & d > 0 & a1 < a2 implies ((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)'])) = (((1 / 2) * d) * ((c + a2) - a1)) * (a1 + a2) )
assume A1: ( c > 0 & d > 0 & a1 < a2 ) ; :: thesis: ((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)'])) = (((1 / 2) * d) * ((c + a2) - a1)) * (a1 + a2)
set f = integral (((id REAL) (#) (AffineMap ((d / c),(- ((d / c) * (a1 - c)))))),['(a1 - c),a1']);
set g = integral (((id REAL) (#) (AffineMap (0,d))),['a1,a2']);
set h = integral (((id REAL) (#) (AffineMap ((- (d / c)),((d / c) * (a2 + c))))),['a2,(a2 + c)']);
B1: ( a1 - c <= a2 - 0 & a2 + 0 <= a2 + c ) by A1, XREAL_1:13, XREAL_1:7;
B2: ( a1 - c <= a1 - 0 & a1 <= a2 ) by A1, XREAL_1:13;
hence ((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 (((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)'])) by INTEGRA5:def 4
.= ((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)'])) by INTEGRA5:def 4, A1
.= ((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))) by INTEGRA5:def 4, B1
.= (((((1 / 3) * (d / c)) * (((a1 * a1) * a1) - (((a1 - c) * (a1 - c)) * (a1 - c)))) + (((1 / 2) * (- ((d / c) * (a1 - c)))) * ((a1 * a1) - ((a1 - c) * (a1 - c))))) + (integral (((id REAL) (#) (AffineMap (0,d))),a1,a2))) + (integral (((id REAL) (#) (AffineMap ((- (d / c)),((d / c) * (a2 + c))))),a2,(a2 + c))) by FUZZY_6:45, B2
.= (((((1 / 3) * (d / c)) * (((a1 * a1) * a1) - (((a1 - c) * (a1 - c)) * (a1 - c)))) + (((1 / 2) * (- ((d / c) * (a1 - c)))) * ((a1 * a1) - ((a1 - c) * (a1 - c))))) + ((((1 / 3) * 0) * (((a2 * a2) * a2) - ((a1 * a1) * a1))) + (((1 / 2) * d) * ((a2 * a2) - (a1 * a1))))) + (integral (((id REAL) (#) (AffineMap ((- (d / c)),((d / c) * (a2 + c))))),a2,(a2 + c))) by FUZZY_6:45, A1
.= ((((((1 / 3) * (d / c)) * (((a1 * a1) * a1) - (((((a1 * a1) - (a1 * c)) - (c * a1)) + (c * c)) * (a1 - c)))) + (((1 / 2) * (- ((d / c) * (a1 - c)))) * ((a1 * a1) - ((((a1 * a1) - (a1 * c)) - (c * a1)) + (c * c))))) + ((((1 / 2) * d) * a2) * a2)) - ((((1 / 2) * d) * a1) * a1)) + ((((1 / 3) * (- (d / c))) * ((((a2 + c) * (a2 + c)) * (a2 + c)) - ((a2 * a2) * a2))) + (((1 / 2) * ((d / c) * (a2 + c))) * (((a2 + c) * (a2 + c)) - (a2 * a2)))) by FUZZY_6:45, B1
.= (((- ((((1 / 2) * (- ((d / c) * c))) * a1) * c)) + ((((1 / 2) * ((d / c) * c)) * a2) * c)) + ((((1 / 2) * d) * a2) * a2)) - ((((1 / 2) * d) * a1) * a1)
.= (((- ((((1 / 2) * (- d)) * a1) * c)) + ((((1 / 2) * ((d / c) * c)) * a2) * c)) + ((((1 / 2) * d) * a2) * a2)) - ((((1 / 2) * d) * a1) * a1) by XCMPLX_1:87, A1
.= ((((((1 / 2) * d) * a1) * c) + ((((1 / 2) * d) * a2) * c)) + ((((1 / 2) * d) * a2) * a2)) - ((((1 / 2) * d) * a1) * a1) by XCMPLX_1:87, A1
.= (((1 / 2) * d) * ((c + a2) - a1)) * (a1 + a2) ;
:: thesis: verum