theorem Th17X: :: FUZZY_6:29

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
( f is_integrable_on A & f | A is bounded )