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