let a1, c, a2, d be Real; :: thesis:
let f be Function of REAL,REAL; :: thesis:
assume that
A1: ( c > 0 & d > 0 & a1 < a2 ) and
A2: f | [.(a1 - c),(a2 + c).] = (((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).]) ; :: thesis:
set g = AffineMap ((- (d / c)),((d / c) * (a2 + c)));
reconsider F = ((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | ].-infty,a1.[) +* ((AffineMap (0,d)) | [.a1,+infty.[) as Function of REAL,REAL by FUZZY_5:74;
B4: (d - (- ((d / c) * (a1 - c)))) / ((d / c) - 0) = (d + ((d / c) * (a1 - c))) / (d / c)
.= (d / (d / c)) + (a1 - c) by XCMPLX_1:113, A1
.= c + (a1 - c) by XCMPLX_1:54, A1
.= a1 ;
then C12: ( F is_integrable_on ['(a1 - c),(a2 + c)'] & F | ['(a1 - c),(a2 + c)'] is bounded ) by FUZZY_6:29, A1;
B2: ( a1 - c <= a1 - 0 & a1 <= a2 ) by A1, XREAL_1:13;
B1: ( a1 - c <= a2 - 0 & a2 + 0 <= a2 + c ) by A1, XREAL_1:13, XREAL_1:7;
then ( [.(lower_bound ['(a1 - c),a2']),(upper_bound ['(a1 - c),a2']).] = ['(a1 - c),a2'] & ['(a1 - c),a2'] = [.(a1 - c),a2.] ) by INTEGRA5:def 3, INTEGRA1:4;
then D1: ( upper_bound ['(a1 - c),a2'] = a2 & lower_bound ['(a1 - c),a2'] = a1 - c ) by INTEGRA1:5;
a1 in [.(a1 - c),a2.] by B2;
then CC: (d - (- ((d / c) * (a1 - c)))) / ((d / c) - 0) in ['(a1 - c),a2'] by B1, INTEGRA5:def 3, B4;
C2: F | [.(a1 - c),a2.] = F | ['(a1 - c),a2'] by INTEGRA5:def 3, B1
.= ((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(a1 - c),a1.]) +* ((AffineMap (0,d)) | [.a1,a2.]) by D1, B4, FUZZY_6:40, CC ;
reconsider tr = d (#) (TrapezoidalFS ((a1 - c),a1,a2,(a2 + c))) as PartFunc of REAL,REAL ;
reconsider f1 = f as PartFunc of REAL,REAL ;
XX: tr | ['(a1 - c),(a2 + c)'] = f1 | [.(a1 - c),(a2 + c).] by A2, SymTrape, A1;
( a1 - c < a1 - 0 & a2 + 0 < a2 + c ) by A1, XREAL_1:15, XREAL_1:8;
then TrapezoidalFS ((a1 - c),a1,a2,(a2 + c)) is continuous by FUZNUM_1:32, A1;
then X1: f1 | ['(a1 - c),(a2 + c)'] is continuous by INTEGRA5:def 3, XX, B1, XXREAL_0:2;
REAL = dom f1 by FUNCT_2:def 1;
then C14: f is_integrable_on ['(a1 - c),(a2 + c)'] by INTEGRA5:11, X1;
C13c: ( ((- (d / c)) * a2) + ((d / c) * (a2 + c)) = (((- (d / c)) * a2) + ((d / c) * a2)) + ((d / c) * c) & (((- (d / c)) * a2) + ((d / c) * a2)) + ((d / c) * c) = d ) by XCMPLX_1:87, A1;
a2 in [.a1,+infty.[ by XXREAL_1:236, A1;
then a2 in dom ((AffineMap (0,d)) | [.a1,+infty.[) by FUNCT_2:def 1;
then C13: F . a2 = ((AffineMap (0,d)) | [.a1,+infty.[) . a2 by FUNCT_4:13
.= (AffineMap (0,d)) . a2 by FUNCT_1:49, XXREAL_1:236, A1
.= (0 * a2) + d by FCONT_1:def 4
.= (AffineMap ((- (d / c)),((d / c) * (a2 + c)))) . a2 by FCONT_1:def 4, C13c ;
C11: ( AffineMap ((- (d / c)),((d / c) * (a2 + c))) is_integrable_on ['(a1 - c),(a2 + c)'] & (AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | ['(a1 - c),(a2 + c)'] is bounded ) by FUZZY_6:41;
C23: (AffineMap ((d / c),(- ((d / c) * (a1 - c))))) . a1 = ((d / c) * a1) + (- ((d / c) * (a1 - c))) by FCONT_1:def 4
.= (((d / c) * a1) + (- ((d / c) * a1))) - (- ((d / c) * c))
.= (0 * a1) + d by XCMPLX_1:87, A1
.= (AffineMap (0,d)) . a1 by FCONT_1:def 4 ;
C22: F is_integrable_on ['(a1 - c),a2'] by FUZZY_6:29, B4, A1;
C21: ( AffineMap ((d / c),(- ((d / c) * (a1 - c)))) is_integrable_on ['(a1 - c),a2'] & (AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | ['(a1 - c),a2'] is bounded & AffineMap (0,d) is_integrable_on ['(a1 - c),a2'] & (AffineMap (0,d)) | ['(a1 - c),a2'] is bounded ) by FUZZY_6:41;
thus integral (f,['(a1 - c),(a2 + c)']) = (integral (F,['(a1 - c),a2'])) + (integral ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))),['a2,(a2 + c)'])) by FUZZY_6:33, B1, C11, C12, C13, C14, A2, C2
.= ((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 FUZZY_6:33, B2, C21, C22, C2, C23 ; :: thesis: