theorem Th23A: :: FUZZY_6:43

for A being non empty closed_interval Subset of REAL
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)']))