let A be non empty closed_interval Subset of REAL; :: thesis: for a, b, c, d being Real
for f being Function of REAL,REAL st c > 0 & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
( f is_integrable_on A & f | A is bounded )
let a, b, c, d be Real; :: thesis: for f being Function of REAL,REAL st c > 0 & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
( f is_integrable_on A & f | A is bounded )
let f be Function of REAL,REAL; :: thesis: ( c > 0 & ( for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ) implies ( f is_integrable_on A & f | A is bounded ) )
assume that
A2: c > 0 and
A3: for x being Real holds f . x = min (d,(max (0,(b - |.((b * (x - a)) / c).|)))) ; :: thesis: ( f is_integrable_on A & f | A is bounded )
reconsider f = f as PartFunc of REAL,REAL ;
f is Lipschitzian by L724, A2, A3;
then A6: f | A is continuous ;
dom f = REAL by FUNCT_2:def 1;
hence ( f is_integrable_on A & f | A is bounded ) by INTEGRA5:11, INTEGRA5:10, A6; :: thesis: verum