let a be Real; :: thesis:
let A be non empty closed_interval Subset of REAL; :: thesis:
let f be Function of A,REAL; :: thesis:
assume A1: for x, y being Real st x in A & y in A holds
|.((f . x) - (f . y)).| <= a ; :: thesis:
A2: for y being Real st y in A holds
(upper_bound (rng f)) - a <= f . y

let y be Real; :: thesis:
assume A3: y in A ; :: thesis:
for b being Real st b in rng f holds
b <= a + (f . y)

let b be Real; :: thesis:
assume b in rng f ; :: thesis:
then consider x being Element of A such that
x in dom f and
A4: b = f . x by PARTFUN1:3;
|.((f . x) - (f . y)).| <= a by A1, A3;
then (f . x) - (f . y) <= a by ABSVALUE:5;
hence b <= a + (f . y) by A4, XREAL_1:20; :: thesis:

end;

then upper_bound (rng f) <= a + (f . y) by SEQ_4:45;
hence (upper_bound (rng f)) - a <= f . y by XREAL_1:20; :: thesis:

end;

for b being Real st b in rng f holds
(upper_bound (rng f)) - a <= b

let b be Real; :: thesis:
assume b in rng f ; :: thesis:
then ex x being Element of A st
( x in dom f & b = f . x ) by PARTFUN1:3;
hence (upper_bound (rng f)) - a <= b by A2; :: thesis:

end;

then (upper_bound (rng f)) - a <= lower_bound (rng f) by SEQ_4:43;
then upper_bound (rng f) <= a + (lower_bound (rng f)) by XREAL_1:20;
hence (upper_bound (rng f)) - (lower_bound (rng f)) <= a by XREAL_1:20; :: thesis: