theorem Th17: :: FUZZY_6:42

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 = ((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) ) )