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 F1 = AffineMap ((d / c),(- ((d / c) * (a1 - c))));
set F2 = AffineMap (0,d);
set F3 = 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_6:18;
set ap = (d - (- ((d / c) * (a1 - c)))) / ((d / c) - 0);
P2: (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 ;
B1: ( a1 - c <= a2 - 0 & a2 + 0 <= a2 + c ) by A1, XREAL_1:13, XREAL_1:7;
then P3f: ( [.(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 P3: ( upper_bound ['(a1 - c),a2'] = a2 & lower_bound ['(a1 - c),a2'] = a1 - c ) by INTEGRA1:5;
( a1 - c <= a1 - 0 & a1 <= a2 ) by A1, XREAL_1:13;
then (d - (- ((d / c) * (a1 - c)))) / ((d / c) - 0) in [.(a1 - c),a2.] by P2;
then P1: (d - (- ((d / c) * (a1 - c)))) / ((d / c) - 0) in ['(a1 - c),a2'] by INTEGRA5:def 3, B1;
F | ['(a1 - c),a2'] = ((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(lower_bound ['(a1 - c),a2']),((d - (- ((d / c) * (a1 - c)))) / ((d / c) - 0)).]) +* ((AffineMap (0,d)) | [.((d - (- ((d / c) * (a1 - c)))) / ((d / c) - 0)),(upper_bound ['(a1 - c),a2']).]) by FUZZY_6:40, P1, P2;
then C1: integral (((id REAL) (#) F),['(a1 - c),a2']) = (integral (((id REAL) (#) (AffineMap ((d / c),(- ((d / c) * (a1 - c)))))),['(a1 - c),a1'])) + (integral (((id REAL) (#) (AffineMap (0,d))),['a1,a2'])) by P2, P3, FUZZY_6:43, P1, A1;
a2 in [.a1,+infty.[ by XXREAL_1:236, A1;
then B4a: a2 in dom ((AffineMap (0,d)) | [.a1,+infty.[) by FUNCT_2:def 1;
B4: (AffineMap ((- (d / c)),((d / c) * (a2 + c)))) . a2 = ((- (d / c)) * a2) + ((d / c) * (a2 + c)) by FCONT_1:def 4
.= (((- (d / c)) * a2) + ((d / c) * a2)) + ((d / c) * c)
.= (0 * a2) + d by A1, XCMPLX_1:87
.= (AffineMap (0,d)) . a2 by FCONT_1:def 4
.= ((AffineMap (0,d)) | [.a1,+infty.[) . a2 by FUNCT_1:49, XXREAL_1:236, A1
.= F . a2 by FUNCT_4:13, B4a ;
B2: F is Lipschitzian by FUZZY_6:28, P2, A1;
(F | [.(a1 - c),a2.]) +* ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]) = (F | ['(a1 - c),a2']) +* ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]) by INTEGRA5:def 3, B1
.= (((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(lower_bound ['(a1 - c),a2']),((d - (- ((d / c) * (a1 - c)))) / ((d / c) - 0)).]) +* ((AffineMap (0,d)) | [.((d - (- ((d / c) * (a1 - c)))) / ((d / c) - 0)),(upper_bound ['(a1 - c),a2']).])) +* ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]) by FUZZY_6:40, P1, P2
.= (((AffineMap ((d / c),(- ((d / c) * (a1 - c))))) | [.(a1 - c),((d - (- ((d / c) * (a1 - c)))) / ((d / c) - 0)).]) +* ((AffineMap (0,d)) | [.((d - (- ((d / c) * (a1 - c)))) / ((d / c) - 0)),(upper_bound ['(a1 - c),a2']).])) +* ((AffineMap ((- (d / c)),((d / c) * (a2 + c)))) | [.a2,(a2 + c).]) by P3f, INTEGRA1:5
.= f | [.(a1 - c),(a2 + c).] by A2, P2, P3f, INTEGRA1:5 ;
hence integral (((id REAL) (#) f),['(a1 - c),(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 C1, Th26p, B1, B2, B4; :: thesis: