theorem Th17C: :: FUZZY_6:40

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 f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) & (q - b) / (a - p) in A holds
f | A = ((AffineMap (a,b)) | [.(lower_bound A),((q - b) / (a - p)).]) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),(upper_bound A).])