let a be Real; :: thesis: for A being non empty 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
|.((h . x) - (h . y)).| <= a * (|.((f . x) - (f . y)).| + |.((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 non empty 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
|.((h . x) - (h . y)).| <= a * (|.((f . x) - (f . y)).| + |.((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
|.((h . x) - (h . y)).| <= a * (|.((f . x) - (f . y)).| + |.((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
|.((h . x) - (h . y)).| <= a * (|.((f . x) - (f . y)).| + |.((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:13;
A6: rng f is bounded_above by A1, INTEGRA1:13;
A7: dom g = A by FUNCT_2:def 1;
A8: rng g is bounded_below by A2, INTEGRA1:11;
A9: for x, y being Real st x in A & y in A holds
|.((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 |.((g . x) - (g . y)).| <= (upper_bound (rng g)) - (lower_bound (rng g)) )
assume that
A10: x in A and
A11: y in A ; :: thesis: |.((g . x) - (g . y)).| <= (upper_bound (rng g)) - (lower_bound (rng g))

now :: thesis: |.((g . x) - (g . y)).| <= (upper_bound (rng g)) - (lower_bound (rng g))

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

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

then (g . x) - (g . y) >= 0 by XREAL_1:48;
then |.((g . x) - (g . y)).| = (g . x) - (g . y) by ABSVALUE:def 1;
then A12: |.((g . x) - (g . y)).| + (g . y) = g . x ;
g . y in rng g by A7, A11, FUNCT_1:def 3;
then A13: lower_bound (rng g) <= g . y by A8, SEQ_4:def 2;
g . x in rng g by A7, A10, FUNCT_1:def 3;
then g . x <= upper_bound (rng g) by A5, SEQ_4:def 1;
then g . y <= (upper_bound (rng g)) - |.((g . x) - (g . y)).| by A12, XREAL_1:19;
then lower_bound (rng g) <= (upper_bound (rng g)) - |.((g . x) - (g . y)).| by A13, XXREAL_0:2;
then (lower_bound (rng g)) + |.((g . x) - (g . y)).| <= upper_bound (rng g) by XREAL_1:19;
hence |.((g . x) - (g . y)).| <= (upper_bound (rng g)) - (lower_bound (rng g)) by XREAL_1:19; :: thesis: verum

end;

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

then (g . x) - (g . y) < 0 by XREAL_1:49;
then |.((g . x) - (g . y)).| = - ((g . x) - (g . y)) by ABSVALUE:def 1
.= (g . y) - (g . x) ;
then A14: |.((g . x) - (g . y)).| + (g . x) = g . y ;
g . x in rng g by A7, A10, FUNCT_1:def 3;
then A15: lower_bound (rng g) <= g . x by A8, SEQ_4:def 2;
g . y in rng g by A7, A11, FUNCT_1:def 3;
then g . y <= upper_bound (rng g) by A5, SEQ_4:def 1;
then g . x <= (upper_bound (rng g)) - |.((g . x) - (g . y)).| by A14, XREAL_1:19;
then lower_bound (rng g) <= (upper_bound (rng g)) - |.((g . x) - (g . y)).| by A15, XXREAL_0:2;
then (lower_bound (rng g)) + |.((g . x) - (g . y)).| <= upper_bound (rng g) by XREAL_1:19;
hence |.((g . x) - (g . y)).| <= (upper_bound (rng g)) - (lower_bound (rng g)) by XREAL_1:19; :: thesis: verum

end;

end;

end;

hence |.((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:11;
A18: for x, y being Real st x in A & y in A holds
|.((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 |.((f . x) - (f . y)).| <= (upper_bound (rng f)) - (lower_bound (rng f)) )
assume that
A19: x in A and
A20: y in A ; :: thesis: |.((f . x) - (f . y)).| <= (upper_bound (rng f)) - (lower_bound (rng f))

now :: thesis: |.((f . x) - (f . y)).| <= (upper_bound (rng f)) - (lower_bound (rng f))

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

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

then (f . x) - (f . y) >= 0 by XREAL_1:48;
then |.((f . x) - (f . y)).| = (f . x) - (f . y) by ABSVALUE:def 1;
then A21: |.((f . x) - (f . y)).| + (f . y) = f . x ;
f . y in rng f by A16, A20, FUNCT_1:def 3;
then A22: lower_bound (rng f) <= f . y by A17, SEQ_4:def 2;
f . x in rng f by A16, A19, FUNCT_1:def 3;
then f . x <= upper_bound (rng f) by A6, SEQ_4:def 1;
then f . y <= (upper_bound (rng f)) - |.((f . x) - (f . y)).| by A21, XREAL_1:19;
then lower_bound (rng f) <= (upper_bound (rng f)) - |.((f . x) - (f . y)).| by A22, XXREAL_0:2;
then (lower_bound (rng f)) + |.((f . x) - (f . y)).| <= upper_bound (rng f) by XREAL_1:19;
hence |.((f . x) - (f . y)).| <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:19; :: thesis: verum

end;

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

then (f . x) - (f . y) < 0 by XREAL_1:49;
then |.((f . x) - (f . y)).| = - ((f . x) - (f . y)) by ABSVALUE:def 1
.= (f . y) - (f . x) ;
then A23: |.((f . x) - (f . y)).| + (f . x) = f . y ;
f . x in rng f by A16, A19, FUNCT_1:def 3;
then A24: lower_bound (rng f) <= f . x by A17, SEQ_4:def 2;
f . y in rng f by A16, A20, FUNCT_1:def 3;
then f . y <= upper_bound (rng f) by A6, SEQ_4:def 1;
then f . x <= (upper_bound (rng f)) - |.((f . x) - (f . y)).| by A23, XREAL_1:19;
then lower_bound (rng f) <= (upper_bound (rng f)) - |.((f . x) - (f . y)).| by A24, XXREAL_0:2;
then (lower_bound (rng f)) + |.((f . x) - (f . y)).| <= upper_bound (rng f) by XREAL_1:19;
hence |.((f . x) - (f . y)).| <= (upper_bound (rng f)) - (lower_bound (rng f)) by XREAL_1:19; :: thesis: verum

end;

end;

end;

hence |.((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
|.((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 |.((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: |.((h . x) - (h . y)).| <= a * (((upper_bound (rng f)) - (lower_bound (rng f))) + ((upper_bound (rng g)) - (lower_bound (rng g))))
A27: a * |.((g . x) - (g . y)).| <= a * ((upper_bound (rng g)) - (lower_bound (rng g))) by A3, A9, A25, A26, XREAL_1:64;
a * |.((f . x) - (f . y)).| <= a * ((upper_bound (rng f)) - (lower_bound (rng f))) by A3, A18, A25, A26, XREAL_1:64;
then A28: (a * |.((f . x) - (f . y)).|) + (a * |.((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:7;
|.((h . x) - (h . y)).| <= a * (|.((f . x) - (f . y)).| + |.((g . x) - (g . y)).|) by A4, A25, A26;
hence |.((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