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 = ((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 )
let a, b, p, q be Real; :: thesis: 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 )
let f be Function of REAL,REAL; :: thesis: ( a <> p & f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) implies ( f is_integrable_on A & f | A is bounded ) )
assume that
A1: a <> p and
A2: f = ((AffineMap (a,b)) | ].-infty,((q - b) / (a - p)).[) +* ((AffineMap (p,q)) | [.((q - b) / (a - p)),+infty.[) ; :: thesis: ( f is_integrable_on A & f | A is bounded )
reconsider f = f as PartFunc of REAL,REAL ;
A3: REAL = dom f by FUNCT_2:def 1;
f is Lipschitzian by Th17L, A1, A2;
then f | A is continuous ;
hence ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11, A3; :: thesis: verum