let A be non empty closed_interval Subset of REAL; :: thesis: for p, q, r, s, t, u being Real
for f being Function of REAL,REAL st p * s < 0 & p > 0 & ( for x being Real holds f . x = max (r,(min (u,((((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x)))) ) holds
( f is_integrable_on A & f | A is bounded )
let p, q, r, s, t, u be Real; :: thesis: for f being Function of REAL,REAL st p * s < 0 & p > 0 & ( for x being Real holds f . x = max (r,(min (u,((((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x)))) ) holds
( f is_integrable_on A & f | A is bounded )
let f be Function of REAL,REAL; :: thesis: ( p * s < 0 & p > 0 & ( for x being Real holds f . x = max (r,(min (u,((((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x)))) ) implies ( f is_integrable_on A & f | A is bounded ) )
assume A1: ( p * s < 0 & p > 0 ) ; :: thesis: ( ex x being Real st not f . x = max (r,(min (u,((((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x)))) or ( f is_integrable_on A & f | A is bounded ) )
assume A2: for x being Real holds f . x = max (r,(min (u,((((AffineMap (p,q)) | ].-infty,((t - q) / (p - s)).]) +* ((AffineMap (s,t)) | [.((t - q) / (p - s)),+infty.[)) . x)))) ; :: thesis: ( f is_integrable_on A & f | A is bounded )
B1: dom f = REAL by FUNCT_2:def 1;
A4: f is Lipschitzian by Th24, A1, A2;
reconsider f = f as PartFunc of REAL,REAL ;
f | A is continuous by A4;
hence ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:10, INTEGRA5:11, B1; :: thesis: verum