let b, c, r be Real; :: thesis: ( b < c implies integral ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))),['b,c']) = (r * (c - b)) / 2 )
set c1 = c - b;
assume A1: b < c ; :: thesis: integral ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))),['b,c']) = (r * (c - b)) / 2
then A7: c - b <> 0 ;
thus integral ((r (#) (AffineMap ((- (1 / (c - b))),(c / (c - b))))),['b,c']) = integral ((AffineMap ((r * (- (1 / (c - b)))),(r * (c / (c - b))))),['b,c']) by FUZZY_7:13
.= (c - b) * ((((r * (- (1 / (c - b)))) * (c + b)) / 2) + (r * (c / (c - b)))) by FUZZY_8:42, A1
.= (c - b) * ((- (((r * (1 / (c - b))) * (c + b)) / 2)) + (r * (c / (c - b))))
.= (c - b) * ((- (((r / (c - b)) * (c + b)) / 2)) + (r * (c / (c - b)))) by XCMPLX_1:99
.= ((c - b) * (- (((r / (c - b)) * (c + b)) / 2))) + ((c - b) * (r * (c / (c - b))))
.= ((c - b) * (- (((r / (c - b)) * (c + b)) / 2))) + ((c - b) * ((r * c) / (c - b))) by XCMPLX_1:74
.= (- ((((c - b) * (r / (c - b))) * (c + b)) / 2)) + (((c - b) * (r * c)) / (c - b)) by XCMPLX_1:74
.= (- (((((c - b) * r) / (c - b)) * (c + b)) / 2)) + (((c - b) * (r * c)) / (c - b)) by XCMPLX_1:74
.= (- ((r * (c + b)) / 2)) + (((c - b) * (r * c)) / (c - b)) by XCMPLX_1:89, A7
.= (- ((r * (c + b)) / 2)) + (r * c) by XCMPLX_1:89, A7
.= (r * (c - b)) / 2 ; :: thesis: verum