let a be Real; :: thesis: for A being closed-interval Subset of REAL
for f, g, h being Function of A,REAL st f | A is bounded & g | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds
(upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g))))
let A be closed-interval Subset of REAL ; :: thesis: for f, g, h being Function of A,REAL st f | A is bounded & g | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) holds
(upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g))))
let f, g, h be Function of A,REAL ; :: thesis: ( f | A is bounded & g | A is bounded & a >= 0 & ( for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ) implies (upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) )
assume that
A1: f | A is bounded and
A2: g | A is bounded and
A3: a >= 0 and
A4: for x, y being Real st x in A & y in A holds
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) ; :: thesis: (upper_bound (rng h)) - (lower_bound (rng h)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g))))
A5: ( dom f = A & dom g = A & dom h = A ) by FUNCT_2:def 1;
( f | A is bounded_below & f | A is bounded_above ) by A1;
then A6: ( rng f is bounded_below & rng f is bounded_above ) by INTEGRA1:13, INTEGRA1:15;
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 ;
A11: ( f . x in rng f & f . y in rng f ) by A5, A8, A9, FUNCT_1:def 5;
then f . x <= upper_bound (rng f) by A6, SEQ_4:def 4;
then A12: f . y <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A10, XREAL_1:21;
lower_bound (rng f) <= f . y by A6, A11, SEQ_4:def 5;
then lower_bound (rng f) <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A12, 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 A13: (abs ((f . x) - (f . y))) + (f . x) = f . y ;
A14: ( f . x in rng f & f . y in rng f ) by A5, A8, A9, FUNCT_1:def 5;
then f . y <= upper_bound (rng f) by A6, SEQ_4:def 4;
then A15: f . x <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A13, XREAL_1:21;
lower_bound (rng f) <= f . x by A6, A14, SEQ_4:def 5;
then lower_bound (rng f) <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A15, 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;

( g | A is bounded_below & g | A is bounded_above ) by A2;
then A16: ( rng g is bounded_below & rng g is bounded_above ) by INTEGRA1:13, INTEGRA1:15;
A17: for x, y being Real st x in A & y in A holds
abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g))

proof

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

now

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

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

then (g . x) - (g . y) >= 0 by XREAL_1:50;
then abs ((g . x) - (g . y)) = (g . x) - (g . y) by ABSVALUE:def 1;
then A20: (abs ((g . x) - (g . y))) + (g . y) = g . x ;
A21: ( g . x in rng g & g . y in rng g ) by A5, A18, A19, FUNCT_1:def 5;
then g . x <= upper_bound (rng g) by A16, SEQ_4:def 4;
then A22: g . y <= (upper_bound (rng g)) - (abs ((g . x) - (g . y))) by A20, XREAL_1:21;
lower_bound (rng g) <= g . y by A16, A21, SEQ_4:def 5;
then lower_bound (rng g) <= (upper_bound (rng g)) - (abs ((g . x) - (g . y))) by A22, XXREAL_0:2;
then (lower_bound (rng g)) + (abs ((g . x) - (g . y))) <= upper_bound (rng g) by XREAL_1:21;
hence abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g)) by XREAL_1:21; :: thesis: verum

end;

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

then (g . x) - (g . y) < 0 by XREAL_1:51;
then abs ((g . x) - (g . y)) = - ((g . x) - (g . y)) by ABSVALUE:def 1
.= (g . y) - (g . x) ;
then A23: (abs ((g . x) - (g . y))) + (g . x) = g . y ;
A24: ( g . x in rng g & g . y in rng g ) by A5, A18, A19, FUNCT_1:def 5;
then g . y <= upper_bound (rng g) by A16, SEQ_4:def 4;
then A25: g . x <= (upper_bound (rng g)) - (abs ((g . x) - (g . y))) by A23, XREAL_1:21;
lower_bound (rng g) <= g . x by A16, A24, SEQ_4:def 5;
then lower_bound (rng g) <= (upper_bound (rng g)) - (abs ((g . x) - (g . y))) by A25, XXREAL_0:2;
then (lower_bound (rng g)) + (abs ((g . x) - (g . y))) <= upper_bound (rng g) by XREAL_1:21;
hence abs ((g . x) - (g . y)) <= (upper_bound (rng g)) - (lower_bound (rng g)) by XREAL_1:21; :: thesis: verum

end;

end;

end;

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

end;

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

proof

let x, y be Real; :: thesis: ( x in A & y in A implies abs ((h . x) - (h . y)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) )
assume that
A26: x in A and
A27: y in A ; :: thesis: abs ((h . x) - (h . y)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g))))
A28: abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) by A4, A26, A27;
A29: a * (abs ((f . x) - (f . y))) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by A3, A7, A26, A27, XREAL_1:66;
a * (abs ((g . x) - (g . y))) <= a * ((upper_bound (rng g)) - (lower_bound (rng g))) by A3, A17, A26, A27, XREAL_1:66;
then (a * (abs ((f . x) - (f . y)))) + (a * (abs ((g . x) - (g . y)))) <= (a * ((upper_bound (rng f)) - (lower_bound (rng f)))) + (a * ((upper_bound (rng g)) - (lower_bound (rng g)))) by A29, XREAL_1:9;
hence abs ((h . x) - (h . y)) <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g)))) by A28, XXREAL_0:2; :: thesis: verum

end;

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