let A be non empty closed_interval Subset of REAL; :: thesis: for a, b, p, q being Real
for f being Function of REAL,REAL st a <> p & f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) holds
( ( (q - b) / (a - p) in A implies integral (f,A) = (integral ((AffineMap (a,b)),['(lower_bound A),((q - b) / (a - p))'])) + (integral ((AffineMap (p,q)),['((q - b) / (a - p)),(upper_bound A)'])) ) & ( (q - b) / (a - p) <= lower_bound A implies integral (f,A) = integral ((AffineMap (p,q)),A) ) & ( (q - b) / (a - p) >= upper_bound A implies integral (f,A) = integral ((AffineMap (a,b)),A) ) )
let a, b, p, q be Real; :: thesis: for f being Function of REAL,REAL st a <> p & f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) holds
( ( (q - b) / (a - p) in A implies integral (f,A) = (integral ((AffineMap (a,b)),['(lower_bound A),((q - b) / (a - p))'])) + (integral ((AffineMap (p,q)),['((q - b) / (a - p)),(upper_bound A)'])) ) & ( (q - b) / (a - p) <= lower_bound A implies integral (f,A) = integral ((AffineMap (p,q)),A) ) & ( (q - b) / (a - p) >= upper_bound A implies integral (f,A) = integral ((AffineMap (a,b)),A) ) )
let f be Function of REAL,REAL; :: thesis: ( a <> p & f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) implies ( ( (q - b) / (a - p) in A implies integral (f,A) = (integral ((AffineMap (a,b)),['(lower_bound A),((q - b) / (a - p))'])) + (integral ((AffineMap (p,q)),['((q - b) / (a - p)),(upper_bound A)'])) ) & ( (q - b) / (a - p) <= lower_bound A implies integral (f,A) = integral ((AffineMap (p,q)),A) ) & ( (q - b) / (a - p) >= upper_bound A implies integral (f,A) = integral ((AffineMap (a,b)),A) ) ) )
assume that
A1: a <> p and
A2: f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) ; :: thesis: ( ( (q - b) / (a - p) in A implies integral (f,A) = (integral ((AffineMap (a,b)),['(lower_bound A),((q - b) / (a - p))'])) + (integral ((AffineMap (p,q)),['((q - b) / (a - p)),(upper_bound A)'])) ) & ( (q - b) / (a - p) <= lower_bound A implies integral (f,A) = integral ((AffineMap (p,q)),A) ) & ( (q - b) / (a - p) >= upper_bound A implies integral (f,A) = integral ((AffineMap (a,b)),A) ) )
B3: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4
.= ['(lower_bound A),(upper_bound A)'] by INTEGRA5:def 3, SEQ_4:11 ;
A4: (AffineMap (a,b)) . ((q - b) / (a - p)) = (AffineMap (p,q)) . ((q - b) / (a - p)) by Th17E, A1;
A5: ( AffineMap (a,b) is_integrable_on ['(lower_bound A),(upper_bound A)'] & (AffineMap (a,b)) | ['(lower_bound A),(upper_bound A)'] is bounded ) by Th17B;
A7: AffineMap (p,q) is_integrable_on ['(lower_bound A),(upper_bound A)'] by Th17B;
A8: (AffineMap (p,q)) | ['(lower_bound A),(upper_bound A)'] is bounded by Th17B;
A11: f is_integrable_on ['(lower_bound A),(upper_bound A)'] by Th17X, A1, A2;
AA: ( (q - b) / (a - p) in A implies integral (f,A) = (integral ((AffineMap (a,b)),['(lower_bound A),((q - b) / (a - p))'])) + (integral ((AffineMap (p,q)),['((q - b) / (a - p)),(upper_bound A)'])) )

proof

assume B1: (q - b) / (a - p) in A ; :: thesis: integral (f,A) = (integral ((AffineMap (a,b)),['(lower_bound A),((q - b) / (a - p))'])) + (integral ((AffineMap (p,q)),['((q - b) / (a - p)),(upper_bound A)']))
A10: f | [.(lower_bound A),(upper_bound A).] = f | A by INTEGRA1:4
.= ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) by Th17C, A2, B1 ;
(q - b) / (a - p) in [.(lower_bound A),(upper_bound A).] by INTEGRA1:4, B1;
then ( lower_bound A <= (q - b) / (a - p) & (q - b) / (a - p) <= upper_bound A ) by XXREAL_1:1;
hence integral (f,A) = (integral ((AffineMap (a,b)),['(lower_bound A),((q - b) / (a - p))'])) + (integral ((AffineMap (p,q)),['((q - b) / (a - p)),(upper_bound A)'])) by Th18Z, A11, A4, A5, A7, A8, A10, B3; :: thesis: verum

end;

BB: ( (q - b) / (a - p) <= lower_bound A implies integral (f,A) = integral ((AffineMap (p,q)),A) )

proof

assume C1: (q - b) / (a - p) <= lower_bound A ; :: thesis: integral (f,A) = integral ((AffineMap (p,q)),A)
reconsider LU = [.(lower_bound A),(upper_bound A).] as non empty closed_interval Subset of REAL by INTEGRA1:4;
C4: LU = A by INTEGRA1:4;
C5: f | LU = f | A by INTEGRA1:4
.= (AffineMap (p,q)) | A by Th17AX, A2, A4, C1
.= (AffineMap (p,q)) | LU by INTEGRA1:4 ;
thus integral (f,A) = integral (f | LU) by C4, INTEGRA5:def 2
.= integral ((AffineMap (p,q)),LU) by INTEGRA5:def 2, C5
.= integral ((AffineMap (p,q)),A) by INTEGRA1:4 ; :: thesis: verum

end;

( (q - b) / (a - p) >= upper_bound A implies integral (f,A) = integral ((AffineMap (a,b)),A) )

proof

assume E1: (q - b) / (a - p) >= upper_bound A ; :: thesis: integral (f,A) = integral ((AffineMap (a,b)),A)
reconsider LU = [.(lower_bound A),(upper_bound A).] as non empty closed_interval Subset of REAL by INTEGRA1:4;
C4: LU = A by INTEGRA1:4;
C5: f | LU = f | A by INTEGRA1:4
.= (AffineMap (a,b)) | A by Th17AX, A2, A4, E1
.= (AffineMap (a,b)) | LU by INTEGRA1:4 ;
thus integral (f,A) = integral (f | LU) by C4, INTEGRA5:def 2
.= integral ((AffineMap (a,b)),LU) by INTEGRA5:def 2, C5
.= integral ((AffineMap (a,b)),A) by INTEGRA1:4 ; :: thesis: verum

end;

hence ( ( (q - b) / (a - p) in A implies integral (f,A) = (integral ((AffineMap (a,b)),['(lower_bound A),((q - b) / (a - p))'])) + (integral ((AffineMap (p,q)),['((q - b) / (a - p)),(upper_bound A)'])) ) & ( (q - b) / (a - p) <= lower_bound A implies integral (f,A) = integral ((AffineMap (p,q)),A) ) & ( (q - b) / (a - p) >= upper_bound A implies integral (f,A) = integral ((AffineMap (a,b)),A) ) ) by AA, BB; :: thesis: verum