let a be Real; :: thesis: for A being closed-interval Subset of REAL
for f, g being Function of A,REAL st f | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds
(upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
let A be closed-interval Subset of REAL; :: thesis: for f, g being Function of A,REAL st f | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) holds
(upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
let f, g be Function of A,REAL; :: thesis: ( f | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ) implies (upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) )
assume that
A1: f | A is bounded and
A2: a >= 0 and
A3: for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) ; :: thesis: (upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
A4: rng f is bounded_above by A1, INTEGRA1:15;
A5: dom f = A by FUNCT_2:def 1;
A6: rng f is bounded_below by A1, INTEGRA1:13;
A7: for x, y being Real st x in A & y in A holds
abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f))

proof

let x, y be Real; :: thesis: ( x in A & y in A implies abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) )
assume that
A8: x in A and
A9: y in A ; :: thesis: abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f))

now

per cases ( f . x >= f . y or f . x < f . y ) ;

suppose f . x >= f . y ; :: thesis: abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f))

then (f . x) - (f . y) >= 0 by XREAL_1:50;
then abs ((f . x) - (f . y)) = (f . x) - (f . y) by ABSVALUE:def 1;
then A10: (abs ((f . x) - (f . y))) + (f . y) = f . x ;
f . y in rng f by A5, A9, FUNCT_1:def 5;
then A11: lower_bound (rng f) <= f . y by A6, SEQ_4:def 5;
f . x in rng f by A5, A8, FUNCT_1:def 5;
then f . x <= upper_bound (rng f) by A4, SEQ_4:def 4;
then f . y <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A10, XREAL_1:21;
then lower_bound (rng f) <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A11, XXREAL_0:2;
then (lower_bound (rng f)) + (abs ((f . x) - (f . y))) <= upper_bound (rng f) by XREAL_1:21;
hence abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:21; :: thesis: verum

end;

suppose f . x < f . y ; :: thesis: abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f))

then (f . x) - (f . y) < 0 by XREAL_1:51;
then abs ((f . x) - (f . y)) = - ((f . x) - (f . y)) by ABSVALUE:def 1
.= (f . y) - (f . x) ;
then A12: (abs ((f . x) - (f . y))) + (f . x) = f . y ;
f . x in rng f by A5, A8, FUNCT_1:def 5;
then A13: lower_bound (rng f) <= f . x by A6, SEQ_4:def 5;
f . y in rng f by A5, A9, FUNCT_1:def 5;
then f . y <= upper_bound (rng f) by A4, SEQ_4:def 4;
then f . x <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A12, XREAL_1:21;
then lower_bound (rng f) <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A13, XXREAL_0:2;
then (lower_bound (rng f)) + (abs ((f . x) - (f . y))) <= upper_bound (rng f) by XREAL_1:21;
hence abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:21; :: thesis: verum

end;

end;

end;

hence abs ((f . x) - (f . y)) <= (upper_bound (rng f)) - (lower_bound (rng f)) ; :: thesis: verum

end;

for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))

proof

let x, y be Real; :: thesis: ( x in A & y in A implies abs ((g . x) - (g . y)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) )
assume that
A14: x in A and
A15: y in A ; :: thesis: abs ((g . x) - (g . y)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
A16: abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) by A3, A14, A15;
a * (abs ((f . x) - (f . y))) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by A2, A7, A14, A15, XREAL_1:66;
hence abs ((g . x) - (g . y)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by A16, XXREAL_0:2; :: thesis: verum

end;

hence (upper_bound (rng g)) - (lower_bound (rng g)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by Th24; :: thesis: verum