let A be non empty closed_interval Subset of REAL; :: thesis: for a, b, c being Real
for f being Function of REAL,REAL st b > 0 & c > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) holds
( f is_integrable_on A & f | A is bounded )
let a, b, c be Real; :: thesis: for f being Function of REAL,REAL st b > 0 & c > 0 & ( for x being Real holds f . x = 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: ( b > 0 & c > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) implies ( f is_integrable_on A & f | A is bounded ) )
assume that
A1: b > 0 and
A2: c > 0 and
A3: for x being Real holds f . x = 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 Th14, A3, A1, A2;
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