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

A16: dom f = A by FUNCT_2:def 1;
A17: rng f is bounded_below by A1, INTEGRA1:13;
A18: 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
A19: x in A and
A20: 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 A21: (abs ((f . x) - (f . y))) + (f . y) = f . x ;
f . y in rng f by A16, A20, FUNCT_1:def 5;
then A22: lower_bound (rng f) <= f . y by A17, SEQ_4:def 5;
f . x in rng f by A16, A19, FUNCT_1:def 5;
then f . x <= upper_bound (rng f) by A6, SEQ_4:def 4;
then f . y <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A21, XREAL_1:21;
then lower_bound (rng f) <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A22, 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 A23: (abs ((f . x) - (f . y))) + (f . x) = f . y ;
f . x in rng f by A16, A19, FUNCT_1:def 5;
then A24: lower_bound (rng f) <= f . x by A17, SEQ_4:def 5;
f . y in rng f by A16, A20, FUNCT_1:def 5;
then f . y <= upper_bound (rng f) by A6, SEQ_4:def 4;
then f . x <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A23, XREAL_1:21;
then lower_bound (rng f) <= (upper_bound (rng f)) - (abs ((f . x) - (f . y))) by A24, 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 ((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
A25: x in A and
A26: 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))))
A27: a * (abs ((g . x) - (g . y))) <= a * ((upper_bound (rng g)) - (lower_bound (rng g))) by A3, A9, A25, A26, XREAL_1:66;
a * (abs ((f . x) - (f . y))) <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by A3, A18, A25, A26, XREAL_1:66;
then A28: (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 A27, XREAL_1:9;
abs ((h . x) - (h . y)) <= a * ((abs ((f . x) - (f . y))) + (abs ((g . x) - (g . y)))) by A4, A25, A26;
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