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 | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) & (q - b) / (a - p) in A holds
integral (((id REAL) (#) f),A) = (integral (((id REAL) (#) (AffineMap (a,b))),['(lower_bound A),((q - b) / (a - p))'])) + (integral (((id REAL) (#) (AffineMap (p,q))),['((q - b) / (a - p)),(upper_bound A)']))
let a, b, p, q be Real; :: thesis: for f being Function of REAL,REAL st a <> p & f | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) & (q - b) / (a - p) in A holds
integral (((id REAL) (#) f),A) = (integral (((id REAL) (#) (AffineMap (a,b))),['(lower_bound A),((q - b) / (a - p))'])) + (integral (((id REAL) (#) (AffineMap (p,q))),['((q - b) / (a - p)),(upper_bound A)']))
let f be Function of REAL,REAL; :: thesis: ( a <> p & f | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) & (q - b) / (a - p) in A implies integral (((id REAL) (#) f),A) = (integral (((id REAL) (#) (AffineMap (a,b))),['(lower_bound A),((q - b) / (a - p))'])) + (integral (((id REAL) (#) (AffineMap (p,q))),['((q - b) / (a - p)),(upper_bound A)'])) )
assume that
A1: a <> p and
A2: f | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) and
A3: (q - b) / (a - p) in A ; :: thesis: integral (((id REAL) (#) f),A) = (integral (((id REAL) (#) (AffineMap (a,b))),['(lower_bound A),((q - b) / (a - p))'])) + (integral (((id REAL) (#) (AffineMap (p,q))),['((q - b) / (a - p)),(upper_bound A)']))
(q - b) / (a - p) in [.(lower_bound A),(upper_bound A).] by INTEGRA1:4, A3;
then B1: ( lower_bound A <= (q - b) / (a - p) & (q - b) / (a - p) <= upper_bound A ) by XXREAL_1:1;
B6: ((id REAL) (#) (AffineMap (a,b))) . ((q - b) / (a - p)) = ((id REAL) . ((q - b) / (a - p))) * ((AffineMap (a,b)) . ((q - b) / (a - p))) by VALUED_1:5
.= ((id REAL) . ((q - b) / (a - p))) * ((AffineMap (p,q)) . ((q - b) / (a - p))) by Th17E, A1
.= ((id REAL) (#) (AffineMap (p,q))) . ((q - b) / (a - p)) by VALUED_1:5 ;
B2: ((id REAL) (#) f) | [.(lower_bound A),(upper_bound A).] = (((id REAL) (#) (AffineMap (a,b))) | [.(lower_bound A),((q - b) / (a - p)).]) +* (((id REAL) (#) (AffineMap (p,q))) | [.((q - b) / (a - p)),(upper_bound A).])

proof

A4: dom (((id REAL) (#) f) | [.(lower_bound A),(upper_bound A).]) = [.(lower_bound A),(upper_bound A).] by FUNCT_2:def 1
.= [.(lower_bound A),((q - b) / (a - p)).] \/ [.((q - b) / (a - p)),(upper_bound A).] by XXREAL_1:165, B1
.= (dom (((id REAL) (#) (AffineMap (a,b))) | [.(lower_bound A),((q - b) / (a - p)).])) \/ [.((q - b) / (a - p)),(upper_bound A).] by FUNCT_2:def 1
.= (dom (((id REAL) (#) (AffineMap (a,b))) | [.(lower_bound A),((q - b) / (a - p)).])) \/ (dom (((id REAL) (#) (AffineMap (p,q))) | [.((q - b) / (a - p)),(upper_bound A).])) by FUNCT_2:def 1
.= dom ((((id REAL) (#) (AffineMap (a,b))) | [.(lower_bound A),((q - b) / (a - p)).]) +* (((id REAL) (#) (AffineMap (p,q))) | [.((q - b) / (a - p)),(upper_bound A).])) by FUNCT_4:def 1 ;
for x being object st x in dom (((id REAL) (#) f) | [.(lower_bound A),(upper_bound A).]) holds
(((id REAL) (#) f) | [.(lower_bound A),(upper_bound A).]) . x = ((((id REAL) (#) (AffineMap (a,b))) | [.(lower_bound A),((q - b) / (a - p)).]) +* (((id REAL) (#) (AffineMap (p,q))) | [.((q - b) / (a - p)),(upper_bound A).])) . x

proof

let x be object ; :: thesis: ( x in dom (((id REAL) (#) f) | [.(lower_bound A),(upper_bound A).]) implies (((id REAL) (#) f) | [.(lower_bound A),(upper_bound A).]) . x = ((((id REAL) (#) (AffineMap (a,b))) | [.(lower_bound A),((q - b) / (a - p)).]) +* (((id REAL) (#) (AffineMap (p,q))) | [.((q - b) / (a - p)),(upper_bound A).])) . x )
assume G8: x in dom (((id REAL) (#) f) | [.(lower_bound A),(upper_bound A).]) ; :: thesis: (((id REAL) (#) f) | [.(lower_bound A),(upper_bound A).]) . x = ((((id REAL) (#) (AffineMap (a,b))) | [.(lower_bound A),((q - b) / (a - p)).]) +* (((id REAL) (#) (AffineMap (p,q))) | [.((q - b) / (a - p)),(upper_bound A).])) . x
G1: x in [.(lower_bound A),(upper_bound A).] by G8;
reconsider x = x as Real by G8;
G3: ( lower_bound A <= x & x <= upper_bound A ) by G8, XXREAL_1:1;
G9: x in A by INTEGRA1:4, G1;

per cases ( x < (q - b) / (a - p) or x >= (q - b) / (a - p) ) ;

suppose G2: x < (q - b) / (a - p) ; :: thesis: (((id REAL) (#) f) | [.(lower_bound A),(upper_bound A).]) . x = ((((id REAL) (#) (AffineMap (a,b))) | [.(lower_bound A),((q - b) / (a - p)).]) +* (((id REAL) (#) (AffineMap (p,q))) | [.((q - b) / (a - p)),(upper_bound A).])) . x

G5: not x in dom (((id REAL) (#) (AffineMap (p,q))) | [.((q - b) / (a - p)),(upper_bound A).]) by G2, XXREAL_1:1;
G10: not x in dom ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) by G2, XXREAL_1:1;
(((id REAL) (#) f) | [.(lower_bound A),(upper_bound A).]) . x = ((id REAL) (#) f) . x by FUNCT_1:49, G8
.= ((id REAL) . x) * (f . x) by VALUED_1:5
.= ((id REAL) . x) * ((((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) . x) by A2, FUNCT_1:49, G9
.= ((id REAL) . x) * (((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) . x) by FUNCT_4:11, G10
.= ((id REAL) . x) * ((AffineMap (a,b)) . x) by FUNCT_1:49, G2, G3, XXREAL_1:1
.= ((id REAL) (#) (AffineMap (a,b))) . x by VALUED_1:5
.= (((id REAL) (#) (AffineMap (a,b))) | [.(lower_bound A),((q - b) / (a - p)).]) . x by FUNCT_1:49, G2, G3, XXREAL_1:1 ;
hence (((id REAL) (#) f) | [.(lower_bound A),(upper_bound A).]) . x = ((((id REAL) (#) (AffineMap (a,b))) | [.(lower_bound A),((q - b) / (a - p)).]) +* (((id REAL) (#) (AffineMap (p,q))) | [.((q - b) / (a - p)),(upper_bound A).])) . x by FUNCT_4:11, G5; :: thesis: verum

end;

suppose P1: x >= (q - b) / (a - p) ; :: thesis: (((id REAL) (#) f) | [.(lower_bound A),(upper_bound A).]) . x = ((((id REAL) (#) (AffineMap (a,b))) | [.(lower_bound A),((q - b) / (a - p)).]) +* (((id REAL) (#) (AffineMap (p,q))) | [.((q - b) / (a - p)),(upper_bound A).])) . x

P2: x in [.((q - b) / (a - p)),(upper_bound A).] by P1, G3;
then G10: x in dom ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) by FUNCT_2:def 1;
G5: x in dom (((id REAL) (#) (AffineMap (p,q))) | [.((q - b) / (a - p)),(upper_bound A).]) by FUNCT_2:def 1, P2;
(((id REAL) (#) f) | [.(lower_bound A),(upper_bound A).]) . x = ((id REAL) (#) f) . x by FUNCT_1:49, G8
.= ((id REAL) . x) * (f . x) by VALUED_1:5
.= ((id REAL) . x) * ((((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])) . x) by A2, FUNCT_1:49, G9
.= ((id REAL) . x) * (((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).]) . x) by FUNCT_4:13, G10
.= ((id REAL) . x) * ((AffineMap (p,q)) . x) by FUNCT_1:49, P1, G3, XXREAL_1:1
.= ((id REAL) (#) (AffineMap (p,q))) . x by VALUED_1:5
.= (((id REAL) (#) (AffineMap (p,q))) | [.((q - b) / (a - p)),(upper_bound A).]) . x by FUNCT_1:49, P1, G3, XXREAL_1:1 ;
hence (((id REAL) (#) f) | [.(lower_bound A),(upper_bound A).]) . x = ((((id REAL) (#) (AffineMap (a,b))) | [.(lower_bound A),((q - b) / (a - p)).]) +* (((id REAL) (#) (AffineMap (p,q))) | [.((q - b) / (a - p)),(upper_bound A).])) . x by FUNCT_4:13, G5; :: thesis: verum

end;

end;

end;

hence ((id REAL) (#) f) | [.(lower_bound A),(upper_bound A).] = (((id REAL) (#) (AffineMap (a,b))) | [.(lower_bound A),((q - b) / (a - p)).]) +* (((id REAL) (#) (AffineMap (p,q))) | [.((q - b) / (a - p)),(upper_bound A).]) by FUNCT_1:2, A4; :: thesis: verum

end;

D3: ( dom ((id REAL) (#) (AffineMap (a,b))) = REAL & dom ((id REAL) (#) (AffineMap (p,q))) = REAL ) by FUNCT_2:def 1;
reconsider Fa = (id REAL) (#) (AffineMap (a,b)) as PartFunc of REAL,REAL ;
reconsider Fp = (id REAL) (#) (AffineMap (p,q)) as PartFunc of REAL,REAL ;
Fa | ['(lower_bound A),(upper_bound A)'] is continuous ;
then B3: ( (id REAL) (#) (AffineMap (a,b)) is_integrable_on ['(lower_bound A),(upper_bound A)'] & ((id REAL) (#) (AffineMap (a,b))) | ['(lower_bound A),(upper_bound A)'] is bounded ) by INTEGRA5:10, INTEGRA5:11, D3;
Fp | ['(lower_bound A),(upper_bound A)'] is continuous ;
then B4: ( (id REAL) (#) (AffineMap (p,q)) is_integrable_on ['(lower_bound A),(upper_bound A)'] & ((id REAL) (#) (AffineMap (p,q))) | ['(lower_bound A),(upper_bound A)'] is bounded ) by INTEGRA5:10, INTEGRA5:11, D3;
set F = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[);
reconsider F = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) as Function of REAL,REAL by Th19;
AA: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4
.= ['(lower_bound A),(upper_bound A)'] by INTEGRA5:def 3, SEQ_4:11 ;
C4: F | ['(lower_bound A),(upper_bound A)'] is integrable by INTEGRA5:def 1, Th17X, A1;
C3: F | ['(lower_bound A),(upper_bound A)'] = f | A by A2, A3, Th17C, AA
.= f | [.(lower_bound A),(upper_bound A).] by INTEGRA1:4
.= f | ['(lower_bound A),(upper_bound A)'] by INTEGRA5:def 3, SEQ_4:11 ;
( f is_integrable_on ['(lower_bound A),(upper_bound A)'] & f | ['(lower_bound A),(upper_bound A)'] is bounded ) by INTEGRA5:def 1, C4, C3, Th17X, A1;
then B5: (id REAL) (#) f is_integrable_on ['(lower_bound A),(upper_bound A)'] by Lm3;
reconsider LU = [.(lower_bound A),(upper_bound A).] as non empty closed_interval Subset of REAL by INTEGRA1:4;
thus integral (((id REAL) (#) f),A) = integral (((id REAL) (#) f),LU) by INTEGRA1:4
.= integral (((id REAL) (#) f),['(lower_bound A),(upper_bound A)']) by INTEGRA5:def 3, SEQ_4:11
.= (integral (((id REAL) (#) (AffineMap (a,b))),['(lower_bound A),((q - b) / (a - p))'])) + (integral (((id REAL) (#) (AffineMap (p,q))),['((q - b) / (a - p)),(upper_bound A)'])) by Th18Z, B1, B2, B3, B4, B5, B6 ; :: thesis: verum