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: ( dom f = A & dom g = A ) by FUNCT_2:def 1;
( f | A is bounded_below & f | A is bounded_above ) by A1;
then A5: ( rng f is bounded_below & rng f is bounded_above ) by INTEGRA1:13, INTEGRA1:15;
A6: 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
A7: x in A and
A8: 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 A9: (abs ((f . x) - (f . y))) + (f . y) = f . x ;
A10: ( f . x in rng f & f . y in rng f ) by A4, A7, A8, FUNCT_1:def 5;
then f . x <= upper_bound (rng f) by A5, SEQ_4:def 4;
then A11: f . y <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A9, XREAL_1:21;
lower_bound (rng f) <= f . y by A5, A10, SEQ_4:def 5;
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 ;
A13: ( f . x in rng f & f . y in rng f ) by A4, A7, A8, FUNCT_1:def 5;
then f . y <= upper_bound (rng f) by A5, SEQ_4:def 4;
then A14: f . x <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A12, XREAL_1:21;
lower_bound (rng f) <= f . x by A5, A13, SEQ_4:def 5;
then lower_bound (rng f) <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A14, 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
A15: x in A and
A16: y in A ; :: thesis: abs ((g . x) - (g . y)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f)))
A17: abs ((g . x) - (g . y)) <= a * (abs ((f . x) - (f . y))) by A3, A15, A16;
a * (abs ((f . x) - (f . y))) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by A2, A6, A15, A16, XREAL_1:66;
hence abs ((g . x) - (g . y)) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by A17, 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